results for zip-dev on /home/simon/w/these/zipperposition/examples/polymorph2.p

problem.path
problem.expected_res
unknown
res
error
rtime
0.028s
stime
0.000s
utime
0.000s
errcode
1
full stdout
unification error: incompatible variables
(subst {})
  unifying `A/25:type` and `A/47:type`, 
  unifying `map A/25 B/27:type` and `map A/47 B/49:type`
  at file '/home/simon/w/these/zipperposition/examples/polymorph2.p': line 8, col 47 to 62
Raised at file "src/core/TypedSTerm.ml", line 1207, characters 29-64
Called from file "src/core/TypedSTerm.ml" (inlined), line 1319, characters 18-1023
Called from file "src/core/TypedSTerm.ml", line 1309, characters 6-29
Called from file "src/core/TypedSTerm.ml" (inlined), line 1432, characters 38-54
Called from file "list.ml" (inlined), line 137, characters 24-31
Called from file "src/core/TypedSTerm.ml" (inlined), line 1432, characters 27-60
Called from file "src/core/TypedSTerm.ml", line 1432, characters 27-60
Called from file "src/core/TypedSTerm.ml" (inlined), line 1319, characters 18-1023
Called from file "src/core/TypedSTerm.ml", line 1309, characters 6-29
Called from file "src/core/TypedSTerm.ml", line 1528, characters 6-56
Called from file "src/core/TypeInference.ml", line 701, characters 11-56
Called from file "src/core/TypeInference.ml", line 507, characters 6-34
Called from file "src/core/TypeInference.ml" (inlined), line 697, characters 19-39
Called from file "list.ml", line 82, characters 20-23
Called from file "list.ml" (inlined), line 80, characters 12-77
Called from file "src/core/TypeInference.ml", line 697, characters 10-41
Called from file "src/core/TypeInference.ml", line 507, characters 6-34
Called from file "src/core/TypeInference.ml", line 607, characters 14-34
Called from file "src/core/TypeInference.ml", line 796, characters 10-30
Called from file "src/core/TypeInference.ml", line 626, characters 21-39
Called from file "src/core/TypeInference.ml", line 183, characters 14-18
Re-raised at file "src/core/TypeInference.ml", line 188, characters 6-13
Called from file "src/core/TypeInference.ml", line 183, characters 14-18
Re-raised at file "src/core/TypeInference.ml", line 188, characters 6-13
Called from file "src/core/TypeInference.ml", line 183, characters 14-18
Re-raised at file "src/core/TypeInference.ml", line 188, characters 6-13
Called from file "src/core/TypeInference.ml" (inlined), line 359, characters 2-13
Called from file "src/core/TypeInference.ml" (inlined), line 439, characters 2-55
Called from file "src/core/TypeInference.ml" (inlined), line 624, characters 6-291
Called from file "src/core/TypeInference.ml" (inlined), line 439, characters 2-55
Called from file "src/core/TypeInference.ml", line 624, characters 6-291
Called from file "src/core/TypeInference.ml", line 804, characters 12-27
Re-raised at file "src/core/TypeInference.ml", line 809, characters 4-11
Called from file "src/core/TypeInference.ml" (inlined), line 828, characters 11-26
Called from file "src/core/TypeInference.ml", line 1110, characters 14-34
Called from file "src/core/TypeInference.ml", line 1142, characters 21-53
Called from file "queue.ml", line 105, characters 6-15
Called from file "src/Iter.ml" (inlined), line 152, characters 27-31
Called from file "src/prover_phases/phases_impl.ml" (inlined), line 138, characters 4-31
Called from file "src/Iter.ml" (inlined), line 76, characters 17-22
Called from file "src/core/TypeInference.ml" (inlined), line 1139, characters 2-198
Called from file "src/core/TypeInference.ml" (inlined), line 1153, characters 6-115
Called from file "src/prover_phases/phases_impl.ml" (inlined), line 132, characters 2-293
Called from file "src/core/TypeInference.ml" (inlined), line 1153, characters 6-115
Called from file "src/prover_phases/phases_impl.ml", line 132, characters 2-293

full stderr

prover config
prover.name
zip-dev
prover.cmd
<unknown>
prover.version
(git branch=master commit=973034f2012cd89e3216cd062b4ab57d44a64a6a)
prover.sat
SZS status (CounterSatisfiable|Satisfiable)
prover.unsat
SZS status (Theorem|Unsatisfiable)
prover.unknown
<none>
prover.timeout
SZS status ResourceOut
prover.tag.gaveup
SZS status GaveUp
prover.memory
<none>