results for zip-dev-check on /home/simon/workspace/zipperposition/../TPTP-v6.1.0/Problems/SWW/SWW533_5.p

problem.path
problem.expected_res
unsat
res
unsat
rtime
1.7s
stime
0.000s
utime
0.000s
errcode
1
full stdout 
done 1016 iterations in 1.681s
SZS status Theorem for '/home/simon/workspace/zipperposition/../TPTP-v6.1.0/Problems/SWW/SWW533_5.p'
SZS output start Refutation

SZS output end Refutation
Error: error in llterm:
cannot find var `X0`
in (ctx :depth 0 :vars )
Raised at file "src/core/Util.ml", line 174, characters 23-48
Called from file "src/proofs/LLTerm.ml", line 619, characters 15-39
Called from file "list.ml", line 92, characters 20-23
Called from file "list.ml", line 92, characters 32-39
Called from file "list.ml", line 92, characters 32-39
Called from file "list.ml", line 92, characters 32-39
Called from file "src/proofs/LLTerm.ml", line 623, characters 14-38
Called from file "list.ml", line 92, characters 20-23
Called from file "list.ml", line 92, characters 32-39
Called from file "list.ml", line 92, characters 32-39
Called from file "src/proofs/LLTerm.ml", line 623, characters 14-38
Called from file "list.ml", line 92, characters 20-23
Called from file "src/proofs/LLTerm.ml", line 669, characters 12-36
Called from file "list.ml", line 92, characters 20-23
Called from file "list.ml", line 92, characters 32-39
Called from file "src/proofs/LLTerm.ml", line 669, characters 12-36
Called from file "list.ml", line 92, characters 20-23
Called from file "src/proofs/LLProof_check.ml", line 102, characters 10-42
Called from file "src/proofs/LLProof_check.ml", line 155, characters 17-55
Called from file "src/proofs/LLProof_check.ml", line 178, characters 16-40
Called from file "list.ml", line 110, characters 12-15
Called from file "list.ml", line 110, characters 12-15
Called from file "list.ml", line 110, characters 12-15
Called from file "list.ml", line 110, characters 12-15
Called from file "src/proofs/LLProof_check.ml", line 206, characters 2-9
Called from file "src/prover_phases/phases_impl.ml", line 501, characters 23-57
Called from file "src/prover_phases/phases.ml", line 116, characters 8-12
Called from file "src/prover_phases/phases.ml", line 116, characters 8-12
Called from file "src/prover_phases/phases.ml", line 208, characters 4-8
full stderr 






prover config












prover.name






zip-dev-check










prover.cmd






<unknown>










prover.version






(git branch=master commit=694a5af00bf39764aef2675ff2a7fdd453780cf9)










prover.sat






SZS status (CounterSatisfiable|Satisfiable)










prover.unsat






SZS status (Theorem|Unsatisfiable)










prover.unknown






<none>










prover.timeout






SZS status ResourceOut










prover.memory






<none>