|
problem.path
|
|
|
problem.expected_res
|
unsat
|
|
res
|
unsat
|
|
rtime
|
0.040s
|
|
stime
|
0.000s
|
|
utime
|
0.000s
|
|
errcode
|
0
|
|
proof_check.res
|
invalid
|
|
proof_check.time
|
0.022s
|
Unsat (0.020/0.000/0.012)
|
prover.name
|
sidekick-dev-p
|
|
prover.cmd
|
<unknown>
|
|
prover.version
|
<unknown>
|
|
prover.sat
|
Sat
|
|
prover.unsat
|
Unsat
|
|
prover.unknown
|
Timeout|Unknown
|
|
prover.timeout
|
<none>
|
|
prover.memory
|
<none>
|
checking proof…
(ERROR[quip.check] proof failed with:
no candidate found for paramodulation { view =
Paramod1 {
rw_with =
{ view = (Named "c1118") };
p =
{ view =
(Bool_c (Eq_e,
[(@ t1117);
y$v3_1517448493_46_op]
))
}}
})
(ERROR[quip.check] proof failed with:
no candidate found for paramodulation { view =
Paramod1 {
rw_with =
{ view = (Named "c1169") };
p =
{ view =
(Bool_c (Eq_e,
[(@ t1168);
y$v3_1517448493_47_op]
))
}}
})
(ERROR[quip.check] proof failed with:
no candidate found for paramodulation { view =
Paramod1 {
rw_with =
{ view = (Named "c1220") };
p =
{ view =
(Bool_c (Eq_e,
[(@ t1219); (@ t1216)]))
}}
})
(ERROR[quip.check] proof failed with:
no candidate found for paramodulation { view =
Paramod1 {
rw_with =
{ view = (Named "c1271") };
p =
{ view =
(Bool_c (Eq_e,
[(@ t1270);
y$v3_1517448493_50_op]
))
}}
})
(ERROR[quip.check] proof failed with:
no candidate found for paramodulation { view =
Paramod1 {
rw_with =
{ view = (Named "c1305") };
p =
{ view =
(Bool_c (Eq_e,
[(@ t1304); y$id51_op]))
}}
})
(ERROR[quip.check] proof failed with:
no candidate found for paramodulation { view =
Paramod1 {
rw_with =
{ view = (Named "c1356") };
p =
{ view =
(Bool_c (Eq_e,
[(@ t1355); y$2113]))
}}
})
(ERROR[quip.check] proof failed with:
no candidate found for paramodulation { view =
Paramod1 {
rw_with =
{ view = (Named "c1392") };
p =
{ view =
(Bool_c (Eq_e,
[(@ t1391); y$2174]))
}}
})
(ERROR[quip.check] proof failed with:
no candidate found for paramodulation { view =
Paramod1 {
rw_with = { view = (Named "c552") };
p =
{ view =
(Bool_c (Eq_e,
[(@ t551); y$a_nok_RClient]))
}}
})
(ERROR[quip.check] proof failed with:
no candidate found for paramodulation { view =
Paramod1 {
rw_with =
{ view = (Named "c1152") };
p =
{ view =
(Bool_c (Eq_e,
[(@ t1151); (¬ y$2101)]))
}}
})
(ERROR[quip.check] proof failed with:
no candidate found for paramodulation { view =
Paramod1 {
rw_with = { view = (Named "c571") };
p =
{ view =
(Bool_c (Eq_e,
[(@ t570); y$a_nok_SClient]))
}}
})
(ERROR[quip.check] proof failed with:
no candidate found for paramodulation { view =
Paramod1 {
rw_with =
{ view = (Named "c1203") };
p =
{ view =
(Bool_c (Eq_e,
[(@ t1202); (¬ y$2104)]))
}}
})
(ERROR[quip.check] proof failed with:
no candidate found for paramodulation { view =
Paramod1 {
rw_with =
{ view = (Named "c1254") };
p =
{ view =
(Bool_c (Eq_e,
[(@ t1253);
y$v3_1517448493_49_op]
))
}}
})
(ERROR[quip.check] proof failed with:
no candidate found for paramodulation { view =
Paramod1 {
rw_with =
{ view = (Named "c1084") };
p =
{ view =
(Bool_c (Eq_e,
[(@ t1083); y$prop]))
}}
})
(ERROR[quip.check] proof failed with:
no candidate found for paramodulation { view =
Paramod1 {
rw_with =
{ view = (Named "c1361") };
p =
{ view =
(Bool_c (Eq_e,
[(@ t1352); y$2112]))
}}
})
(ERROR[quip.check] proof failed with:
no candidate found for paramodulation { view =
Paramod1 {
rw_with =
{ view = (Named "c1339") };
p =
{ view =
(Bool_c (Eq_e,
[(@ t1338); (¬ y$2112)]))
}}
})
; { n_valid = 210; n_invalid = 38; n_steps = 248 }
FAIL
; bad steps: c1511, c1514, c1516, c1519, c1522, c1526, c1527, c1528
; done in 0.013s