%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SWC200-1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n006.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 03:08:50 PM UTC 2026
% Result : Unsatisfiable 141.20s 28.06s
% Output : CNFRefutation 141.20s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named f243ERROR: Could not build tree for root c_205979ERROR: MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(f8,axiom,
ssList(nil),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause8) ).
fof(f9,axiom,
ssItem(skac3),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause9) ).
fof(f12,axiom,
! [X0] : ssItem(skaf83(X0)),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause12) ).
fof(f13,axiom,
! [X0] : ssList(skaf82(X0)),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause13) ).
fof(f47,axiom,
! [X0] : ssItem(skaf44(X0)),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause47) ).
fof(f51,axiom,
! [X0,X1] : ssList(skaf45(X0,X1)),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause51) ).
fof(f60,axiom,
! [X0] :
( frontsegP(X0,nil)
| ~ ssList(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause60) ).
fof(f71,axiom,
! [X0] :
( ~ ssItem(X0)
| ~ memberP(nil,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause71) ).
fof(f86,axiom,
! [X0,X1] :
( ssList(cons(X0,X1))
| ~ ssList(X1)
| ~ ssItem(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause86) ).
fof(f100,axiom,
! [X0,X1] :
( ~ ssList(X1)
| ~ ssItem(X0)
| cons(X0,X1) != X1 ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause99) ).
fof(f103,axiom,
! [X0] :
( cons(skaf44(X0),nil) = X0
| ~ ssList(X0)
| ~ singletonP(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause101) ).
fof(f112,axiom,
! [X0] :
( nil = X0
| cons(skaf83(X0),skaf82(X0)) = X0
| ~ ssList(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause109) ).
fof(f143,axiom,
! [X0,X1] :
( app(X1,skaf45(X0,X1)) = X0
| ~ ssList(X0)
| ~ ssList(X1)
| ~ frontsegP(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause132) ).
fof(f151,axiom,
! [X2,X0,X1] :
( memberP(app(X0,X2),X1)
| ~ ssItem(X1)
| ~ ssList(X0)
| ~ ssList(X2)
| ~ memberP(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause140) ).
fof(f173,axiom,
! [X2,X0,X1] :
( X2 = X0
| memberP(X1,X2)
| ~ ssItem(X2)
| ~ ssItem(X0)
| ~ ssList(X1)
| ~ memberP(cons(X0,X1),X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause161) ).
fof(f174,plain,
! [X2,X0,X1] :
( X0 = X2
| memberP(X1,X2)
| ~ ssItem(X2)
| ~ ssItem(X0)
| ~ ssList(X1)
| ~ memberP(cons(X0,X1),X2) ),
inference(reorient_equations,[],[f173]) ).
fof(f202,negated_conjecture,
ssList(sk3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_3) ).
fof(f203,negated_conjecture,
ssList(sk4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_4) ).
fof(f205,negated_conjecture,
sk1 = sk3,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_6) ).
fof(f206,negated_conjecture,
singletonP(sk3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_7) ).
fof(f207,negated_conjecture,
! [X0] :
( ssItem(sk5(X0))
| ~ ssItem(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_8) ).
fof(f208,negated_conjecture,
! [X0] :
( memberP(sk1,sk5(X0))
| ~ ssItem(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_9) ).
fof(f209,negated_conjecture,
! [X0] :
( X0 != sk5(X0)
| ~ ssItem(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_10) ).
fof(f210,plain,
! [X0] :
( sk5(X0) != X0
| ~ ssItem(X0) ),
inference(reorient_equations,[],[f209]) ).
fof(f213,plain,
! [X0] :
( memberP(sk3,sk5(X0))
| ~ ssItem(X0) ),
inference(definition_unfolding,[],[f208,f205]) ).
tcf(c_251,plain,
ssList(nil),
inference(cnf_transformation,[],[f8]) ).
tcf(c_252,plain,
ssItem(skac3),
inference(cnf_transformation,[],[f9]) ).
tcf(c_255,plain,
! [X0: $i] : ssItem(skaf83(X0)),
inference(cnf_transformation,[],[f12]) ).
tcf(c_256,plain,
! [X0: $i] : ssList(skaf82(X0)),
inference(cnf_transformation,[],[f13]) ).
tcf(c_290,plain,
! [X0: $i] : ssItem(skaf44(X0)),
inference(cnf_transformation,[],[f47]) ).
tcf(c_294,plain,
! [X0: $i,X1: $i] : ssList(skaf45(X0,X1)),
inference(cnf_transformation,[],[f51]) ).
tcf(c_303,plain,
! [X0: $i] :
( frontsegP(X0,nil)
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f60]) ).
tcf(c_314,plain,
! [X0: $i] :
( ~ ssItem(X0)
| ~ memberP(nil,X0) ),
inference(cnf_transformation,[],[f71]) ).
tcf(c_329,plain,
! [X0: $i,X1: $i] :
( ssList(cons(X1,X0))
| ~ ssItem(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f86]) ).
tcf(c_342,plain,
! [X0: $i,X1: $i] :
( ~ ssItem(X0)
| ~ ssList(X1)
| ( cons(X0,X1) != X1 ) ),
inference(cnf_transformation,[],[f100]) ).
tcf(c_344,plain,
! [X0: $i] :
( ( cons(skaf44(X0),nil) = X0 )
| ~ singletonP(X0)
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f103]) ).
tcf(c_352,plain,
! [X0: $i] :
( ( X0 = nil )
| ( cons(skaf83(X0),skaf82(X0)) = X0 )
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f112]) ).
tcf(c_375,plain,
! [X0: $i,X1: $i] :
( ( app(X1,skaf45(X0,X1)) = X0 )
| ~ ssList(X1)
| ~ ssList(X0)
| ~ frontsegP(X0,X1) ),
inference(cnf_transformation,[],[f143]) ).
tcf(c_381,plain,
! [X0: $i,X1: $i] :
( memberP(cons(X1,X0),X1)
| ~ ssItem(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f241]) ).
tcf(c_383,plain,
! [X0: $i,X1: $i,X2: $i] :
( memberP(app(X0,X2),X1)
| ~ ssItem(X1)
| ~ ssList(X2)
| ~ ssList(X0)
| ~ memberP(X0,X1) ),
inference(cnf_transformation,[],[f151]) ).
tcf(c_404,plain,
! [X0: $i,X1: $i,X2: $i] :
( memberP(X1,X2)
| ( X0 = X2 )
| ~ ssItem(X2)
| ~ ssItem(X0)
| ~ ssList(X1)
| ~ memberP(cons(X0,X1),X2) ),
inference(cnf_transformation,[],[f174]) ).
tcf(c_421,plain,
! [X0: $i,X1: $i,X2: $i] :
( frontsegP(cons(X2,X0),cons(X2,X1))
| ~ ssItem(X2)
| ~ ssList(X1)
| ~ ssList(X0)
| ~ frontsegP(X0,X1) ),
inference(cnf_transformation,[],[f243]) ).
tcf(c_431,negated_conjecture,
ssList(sk3),
inference(cnf_transformation,[],[f202]) ).
tcf(c_432,negated_conjecture,
ssList(sk4),
inference(cnf_transformation,[],[f203]) ).
tcf(c_433,negated_conjecture,
singletonP(sk3),
inference(cnf_transformation,[],[f206]) ).
tcf(c_434,negated_conjecture,
! [X0: $i] :
( ssItem(sk5(X0))
| ~ ssItem(X0) ),
inference(cnf_transformation,[],[f207]) ).
tcf(c_435,negated_conjecture,
! [X0: $i] :
( memberP(sk3,sk5(X0))
| ~ ssItem(X0) ),
inference(cnf_transformation,[],[f213]) ).
tcf(c_436,negated_conjecture,
! [X0: $i] :
( ~ ssItem(X0)
| ( sk5(X0) != X0 ) ),
inference(cnf_transformation,[],[f210]) ).
tcf(c_9914,plain,
( ssItem(sk5(skac3))
| ~ ssItem(skac3) ),
inference(instantiation,[status(thm)],[c_434]) ).
tcf(c_14893,plain,
( ( cons(skaf44(sk3),nil) = sk3 )
| ~ ssList(sk3) ),
inference(superposition,[status(thm)],[c_433,c_344]) ).
tcf(c_14895,plain,
cons(skaf44(sk3),nil) = sk3,
inference(forward_subsumption_resolution,[status(thm)],[c_14893,c_431]) ).
tcf(c_20845,plain,
! [X0: $i] :
( frontsegP(cons(skaf44(sk3),X0),sk3)
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssItem(skaf44(sk3))
| ~ frontsegP(X0,nil) ),
inference(superposition,[status(thm)],[c_14895,c_421]) ).
tcf(c_20851,plain,
! [X0: $i] :
( frontsegP(cons(skaf44(sk3),X0),sk3)
| ~ ssList(X0)
| ~ frontsegP(X0,nil) ),
inference(forward_subsumption_resolution,[status(thm)],[c_20845,c_251,c_290]) ).
tcf(c_21672,plain,
( ( cons(skaf44(sk3),nil) = sk3 )
| ~ ssList(sk3) ),
inference(superposition,[status(thm)],[c_433,c_344]) ).
tcf(c_21674,plain,
cons(skaf44(sk3),nil) = sk3,
inference(forward_subsumption_resolution,[status(thm)],[c_21672,c_431]) ).
tcf(c_25659,plain,
! [X0: $i] :
( memberP(nil,X0)
| ( skaf44(sk3) = X0 )
| ~ ssList(nil)
| ~ ssItem(X0)
| ~ ssItem(skaf44(sk3))
| ~ memberP(sk3,X0) ),
inference(superposition,[status(thm)],[c_21674,c_404]) ).
tcf(c_25664,plain,
! [X0: $i] :
( memberP(nil,X0)
| ( skaf44(sk3) = X0 )
| ~ ssItem(X0)
| ~ memberP(sk3,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_25659,c_251,c_290]) ).
tcf(c_74118,plain,
( ~ ssItem(sk5(skac3))
| ( sk5(sk5(skac3)) != sk5(skac3) ) ),
inference(instantiation,[status(thm)],[c_436]) ).
tcf(c_109975,plain,
( ( cons(skaf44(sk3),nil) = sk3 )
| ~ ssList(sk3) ),
inference(superposition,[status(thm)],[c_433,c_344]) ).
tcf(c_109977,plain,
cons(skaf44(sk3),nil) = sk3,
inference(forward_subsumption_resolution,[status(thm)],[c_109975,c_431]) ).
tcf(c_110008,plain,
( ~ ssList(nil)
| ~ ssItem(skaf44(sk3))
| ( sk3 != nil ) ),
inference(superposition,[status(thm)],[c_109977,c_342]) ).
tcf(c_110017,plain,
sk3 != nil,
inference(forward_subsumption_resolution,[status(thm)],[c_110008,c_251,c_290]) ).
tcf(c_112126,plain,
! [X0: $i] :
( frontsegP(cons(skaf44(sk3),X0),sk3)
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssItem(skaf44(sk3))
| ~ frontsegP(X0,nil) ),
inference(superposition,[status(thm)],[c_109977,c_421]) ).
tcf(c_112132,plain,
! [X0: $i] :
( frontsegP(cons(skaf44(sk3),X0),sk3)
| ~ ssList(X0)
| ~ frontsegP(X0,nil) ),
inference(forward_subsumption_resolution,[status(thm)],[c_112126,c_251,c_290]) ).
tcf(c_122207,plain,
! [X0: $i] :
( frontsegP(cons(skaf44(sk3),X0),sk3)
| ~ ssList(X0) ),
inference(global_subsumption_just,[status(thm)],[c_112132,c_303,c_20851]) ).
tcf(c_122214,plain,
! [X0: $i] :
( ( app(sk3,skaf45(cons(skaf44(sk3),X0),sk3)) = cons(skaf44(sk3),X0) )
| ~ ssList(sk3)
| ~ ssList(X0)
| ~ ssList(cons(skaf44(sk3),X0)) ),
inference(superposition,[status(thm)],[c_122207,c_375]) ).
tcf(c_122218,plain,
! [X0: $i] :
( ( app(sk3,skaf45(cons(skaf44(sk3),X0),sk3)) = cons(skaf44(sk3),X0) )
| ~ ssList(X0)
| ~ ssList(cons(skaf44(sk3),X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_122214,c_431]) ).
tcf(c_174792,plain,
! [X0: $i] :
( ( app(sk3,skaf45(cons(skaf44(sk3),X0),sk3)) = cons(skaf44(sk3),X0) )
| ~ ssList(X0)
| ~ ssItem(skaf44(sk3)) ),
inference(superposition,[status(thm)],[c_329,c_122218]) ).
tcf(c_174795,plain,
! [X0: $i] :
( ( app(sk3,skaf45(cons(skaf44(sk3),X0),sk3)) = cons(skaf44(sk3),X0) )
| ~ ssList(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_174792,c_290]) ).
tcf(c_184157,plain,
( ( cons(skaf44(sk3),nil) = sk3 )
| ~ ssList(sk3) ),
inference(superposition,[status(thm)],[c_433,c_344]) ).
tcf(c_184159,plain,
cons(skaf44(sk3),nil) = sk3,
inference(forward_subsumption_resolution,[status(thm)],[c_184157,c_431]) ).
tcf(c_184542,plain,
( ( sk3 = nil )
| ( cons(skaf83(sk3),skaf82(sk3)) = sk3 ) ),
inference(superposition,[status(thm)],[c_431,c_352]) ).
tcf(c_184575,plain,
cons(skaf83(sk3),skaf82(sk3)) = sk3,
inference(forward_subsumption_resolution,[status(thm)],[c_184542,c_110017]) ).
tcf(c_186117,plain,
! [X0: $i] :
( frontsegP(cons(skaf44(sk3),X0),sk3)
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssItem(skaf44(sk3))
| ~ frontsegP(X0,nil) ),
inference(superposition,[status(thm)],[c_184159,c_421]) ).
tcf(c_186123,plain,
! [X0: $i] :
( frontsegP(cons(skaf44(sk3),X0),sk3)
| ~ ssList(X0)
| ~ frontsegP(X0,nil) ),
inference(forward_subsumption_resolution,[status(thm)],[c_186117,c_251,c_290]) ).
tcf(c_196896,plain,
! [X0: $i] :
( frontsegP(cons(skaf44(sk3),X0),sk3)
| ~ ssList(X0) ),
inference(global_subsumption_just,[status(thm)],[c_186123,c_122207]) ).
tcf(c_196902,plain,
! [X0: $i] :
( ( app(sk3,skaf45(cons(skaf44(sk3),X0),sk3)) = cons(skaf44(sk3),X0) )
| ~ ssList(sk3)
| ~ ssList(X0)
| ~ ssList(cons(skaf44(sk3),X0)) ),
inference(superposition,[status(thm)],[c_196896,c_375]) ).
tcf(c_196906,plain,
! [X0: $i] :
( ( app(sk3,skaf45(cons(skaf44(sk3),X0),sk3)) = cons(skaf44(sk3),X0) )
| ~ ssList(X0)
| ~ ssList(cons(skaf44(sk3),X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_196902,c_431]) ).
tcf(c_197250,plain,
! [X0: $i] :
( ( app(sk3,skaf45(cons(skaf44(sk3),X0),sk3)) = cons(skaf44(sk3),X0) )
| ~ ssList(X0) ),
inference(global_subsumption_just,[status(thm)],[c_196906,c_174795]) ).
tcf(c_197255,plain,
app(sk3,skaf45(cons(skaf44(sk3),sk4),sk3)) = cons(skaf44(sk3),sk4),
inference(superposition,[status(thm)],[c_432,c_197250]) ).
tcf(c_197538,plain,
( memberP(sk3,skaf83(sk3))
| ~ ssItem(skaf83(sk3))
| ~ ssList(skaf82(sk3)) ),
inference(superposition,[status(thm)],[c_184575,c_381]) ).
tcf(c_197565,plain,
memberP(sk3,skaf83(sk3)),
inference(forward_subsumption_resolution,[status(thm)],[c_197538,c_255,c_256]) ).
tcf(c_197714,plain,
! [X0: $i] :
( memberP(cons(skaf44(sk3),sk4),X0)
| ~ ssList(sk3)
| ~ ssItem(X0)
| ~ memberP(sk3,X0)
| ~ ssList(skaf45(cons(skaf44(sk3),sk4),sk3)) ),
inference(superposition,[status(thm)],[c_197255,c_383]) ).
tcf(c_197732,plain,
! [X0: $i] :
( memberP(cons(skaf44(sk3),sk4),X0)
| ~ ssItem(X0)
| ~ memberP(sk3,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_197714,c_431,c_294]) ).
tcf(c_200374,plain,
! [X0: $i] :
( memberP(sk4,X0)
| ( skaf44(sk3) = X0 )
| ~ ssList(sk4)
| ~ ssItem(X0)
| ~ ssItem(skaf44(sk3))
| ~ memberP(sk3,X0) ),
inference(superposition,[status(thm)],[c_197732,c_404]) ).
tcf(c_200375,plain,
! [X0: $i] :
( memberP(sk4,X0)
| ( skaf44(sk3) = X0 )
| ~ ssItem(X0)
| ~ memberP(sk3,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_200374,c_432,c_290]) ).
tcf(c_200560,plain,
! [X0: $i] :
( ~ memberP(sk3,X0)
| ~ ssItem(X0)
| ( skaf44(sk3) = X0 ) ),
inference(global_subsumption_just,[status(thm)],[c_200375,c_314,c_25664]) ).
tcf(c_200561,plain,
! [X0: $i] :
( ( skaf44(sk3) = X0 )
| ~ ssItem(X0)
| ~ memberP(sk3,X0) ),
inference(renaming,[status(thm)],[c_200560]) ).
tcf(c_200566,plain,
! [X0: $i] :
( ( sk5(X0) = skaf44(sk3) )
| ~ ssItem(X0)
| ~ ssItem(sk5(X0)) ),
inference(superposition,[status(thm)],[c_435,c_200561]) ).
tcf(c_200569,plain,
( ( skaf83(sk3) = skaf44(sk3) )
| ~ ssItem(skaf83(sk3)) ),
inference(superposition,[status(thm)],[c_197565,c_200561]) ).
tcf(c_200570,plain,
skaf83(sk3) = skaf44(sk3),
inference(forward_subsumption_resolution,[status(thm)],[c_200569,c_255]) ).
tcf(c_200572,plain,
! [X0: $i] :
( ( sk5(X0) = skaf44(sk3) )
| ~ ssItem(X0) ),
inference(global_subsumption_just,[status(thm)],[c_200566,c_434,c_200566]) ).
tcf(c_200575,plain,
! [X0: $i] :
( ( sk5(X0) = skaf83(sk3) )
| ~ ssItem(X0) ),
inference(light_normalisation,[status(thm)],[c_200572,c_200570]) ).
tcf(c_200582,plain,
sk5(skac3) = skaf83(sk3),
inference(superposition,[status(thm)],[c_252,c_200575]) ).
tcf(c_200584,plain,
! [X0: $i] : sk5(skaf83(X0)) = skaf83(sk3),
inference(superposition,[status(thm)],[c_255,c_200575]) ).
tcf(c_200614,plain,
! [X0: $i] : sk5(skaf83(X0)) = sk5(skac3),
inference(light_normalisation,[status(thm)],[c_200584,c_200582]) ).
tcf(c_205973,plain,
sk5(sk5(skac3)) = sk5(skac3),
inference(superposition,[status(thm)],[c_200582,c_200614]) ).
tcf(c_205979,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_205973,c_74118,c_9914,c_252]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWC200-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.10/5.99 % Computer : n006.cluster.edu
% 0.10/5.99 % Model : x86_64 x86_64
% 0.10/5.99 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.99 % Memory : 8046.5625MB
% 0.10/5.99 % OS : Linux 6.8.0-71-generic
% 0.10/5.99 % CPULimit : 300
% 0.10/5.99 % WCLimit : 300
% 0.10/5.99 % DateTime : Thu Sep 24 16:56:49 UTC 2026
% 0.10/5.99 % CPUTime :
% 0.10/5.99 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.10/6.03 Running first-order theorem proving
% 0.10/6.03 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/6.04
% 0.10/6.04 % ======== iProver multi-core TPTP/SMT =========
% 0.10/6.04
% 0.10/6.04 % Detected problem language: tptp
% 0.16/6.06 % Proving...
% 141.20/28.06 % SZS status Started for theBenchmark.p
% 141.20/28.06 % SZS status Unsatisfiable for theBenchmark.p
% 141.20/28.06
% 141.20/28.06 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 141.20/28.06
% 141.20/28.06 % ------ iProver source info
% 141.20/28.06
% 141.20/28.06 % git: date: 2026-07-19 20:42:38 +0200
% 141.20/28.06 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 141.20/28.06 % git: non_committed_changes: false
% 141.20/28.06
% 141.20/28.06 % ------ Parsing...% successful
% 141.20/28.06
% 141.20/28.06
% 141.20/28.06 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 141.20/28.06
% 141.20/28.06 % ------ Preprocessing... sup_sim: 0 sf_s rm: 1 0s sf_e pe_s pe:1:0s pe_e sup_sim: 0 sf_s rm: 1 0s sf_e pe_s pe_e %
% 141.20/28.06
% 141.20/28.06 % ------ Preprocessing... gs_s sp: 2 0s gs_e snvd_s sp: 0 0s snvd_e %
% 141.20/28.06
% 141.20/28.06 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 141.20/28.06 % ------ Proving...
% 141.20/28.06 % ------ Problem Properties
% 141.20/28.06
% 141.20/28.06 %
% 141.20/28.06 % clauses 183
% 141.20/28.06 % conjectures 6
% 141.20/28.06 % EPR 55
% 141.20/28.06 % Horn 155
% 141.20/28.06 % unary 61
% 141.20/28.06 % binary 24
% 141.20/28.06 % lits 550
% 141.20/28.06 % lits eq 70
% 141.20/28.06 % fd_pure 0
% 141.20/28.06 % fd_pseudo 0
% 141.20/28.06 % fd_cond 15
% 141.20/28.06 % fd_pseudo_cond 14
% 141.20/28.06 % AC symbols 0
% 141.20/28.06
% 141.20/28.06 % ------ Input Options Time Limit: Unbounded
% 141.20/28.06
% 141.20/28.06
% 141.20/28.06 % ------
% 141.20/28.06 % Current options:
% 141.20/28.06 % ------
% 141.20/28.06
% 141.20/28.06
% 141.20/28.06 %
% 141.20/28.06
% 141.20/28.06 % ------ Proving...
% 141.20/28.06 %
% 141.20/28.06
% 141.20/28.06 % SZS status Unsatisfiable for theBenchmark.p
% 141.20/28.06
% 141.20/28.06 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 141.20/28.06
% 141.20/28.06
%------------------------------------------------------------------------------