%------------------------------------------------------------------------------ % File : Prover9---1109a % Problem : SWX241-1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : tptp2X_and_run_prover9 %d %s % Computer : n010.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Wed Apr 29 02:38:10 PM UTC 2026 % Result : Unsatisfiable 12.12s 12.41s % Output : Refutation 12.12s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWX241-1 : TPTP v9.3.0. Released v9.3.0. % 0.12/0.13 % Command : tptp2X_and_run_prover9 %d %s % 0.17/0.34 % Computer : n010.cluster.edu % 0.17/0.34 % Model : x86_64 x86_64 % 0.17/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.17/0.34 % Memory : 8042.1875MB % 0.17/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.17/0.34 % CPULimit : 300 % 0.17/0.34 % WCLimit : 300 % 0.17/0.34 % DateTime : Wed Apr 29 03:08:50 EDT 2026 % 0.17/0.34 % CPUTime : % 3.76/4.12 ============================== Prover9 =============================== % 3.76/4.12 Prover9 (32) version 2009-11A, November 2009. % 3.76/4.12 Process 24907 was started by sandbox on n010.cluster.edu, % 3.76/4.12 Wed Apr 29 03:08:51 2026 % 3.76/4.12 The command was "/export/starexec/sandbox/solver/bin/prover9 -t 300 -f /tmp/Prover9_24754_n010.cluster.edu". % 3.76/4.12 ============================== end of head =========================== % 3.76/4.12 % 3.76/4.12 ============================== INPUT ================================= % 3.76/4.12 % 3.76/4.12 % Reading from file /tmp/Prover9_24754_n010.cluster.edu % 3.76/4.12 % 3.76/4.12 set(prolog_style_variables). % 3.76/4.12 set(auto2). % 3.76/4.12 % set(auto2) -> set(auto). % 3.76/4.12 % set(auto) -> set(auto_inference). % 3.76/4.12 % set(auto) -> set(auto_setup). % 3.76/4.12 % set(auto_setup) -> set(predicate_elim). % 3.76/4.12 % set(auto_setup) -> assign(eq_defs, unfold). % 3.76/4.12 % set(auto) -> set(auto_limits). % 3.76/4.12 % set(auto_limits) -> assign(max_weight, "100.000"). % 3.76/4.12 % set(auto_limits) -> assign(sos_limit, 20000). % 3.76/4.12 % set(auto) -> set(auto_denials). % 3.76/4.12 % set(auto) -> set(auto_process). % 3.76/4.12 % set(auto2) -> assign(new_constants, 1). % 3.76/4.12 % set(auto2) -> assign(fold_denial_max, 3). % 3.76/4.12 % set(auto2) -> assign(max_weight, "200.000"). % 3.76/4.12 % set(auto2) -> assign(max_hours, 1). % 3.76/4.12 % assign(max_hours, 1) -> assign(max_seconds, 3600). % 3.76/4.12 % set(auto2) -> assign(max_seconds, 0). % 3.76/4.12 % set(auto2) -> assign(max_minutes, 5). % 3.76/4.12 % assign(max_minutes, 5) -> assign(max_seconds, 300). % 3.76/4.12 % set(auto2) -> set(sort_initial_sos). % 3.76/4.12 % set(auto2) -> assign(sos_limit, -1). % 3.76/4.12 % set(auto2) -> assign(lrs_ticks, 3000). % 3.76/4.12 % set(auto2) -> assign(max_megs, 400). % 3.76/4.12 % set(auto2) -> assign(stats, some). % 3.76/4.12 % set(auto2) -> clear(echo_input). % 3.76/4.12 % set(auto2) -> set(quiet). % 3.76/4.12 % set(auto2) -> clear(print_initial_clauses). % 3.76/4.12 % set(auto2) -> clear(print_given). % 3.76/4.12 assign(lrs_ticks,-1). % 3.76/4.12 assign(sos_limit,10000). % 3.76/4.12 assign(order,kbo). % 3.76/4.12 set(lex_order_vars). % 3.76/4.12 clear(print_given). % 3.76/4.12 % 3.76/4.12 % formulas(sos). % not echoed (100 formulas) % 3.76/4.12 % 3.76/4.12 ============================== end of input ========================== % 3.76/4.12 % 3.76/4.12 % From the command line: assign(max_seconds, 300). % 3.76/4.12 % 3.76/4.12 ============================== PROCESS NON-CLAUSAL FORMULAS ========== % 3.76/4.12 % 3.76/4.12 % Formulas that are not ordinary clauses: % 3.76/4.12 % 3.76/4.12 ============================== end of process non-clausal formulas === % 3.76/4.12 % 3.76/4.12 ============================== PROCESS INITIAL CLAUSES =============== % 3.76/4.12 % 3.76/4.12 ============================== PREDICATE ELIMINATION ================= % 3.76/4.12 % 3.76/4.12 ============================== end predicate elimination ============= % 3.76/4.12 % 3.76/4.12 Auto_denials: % 3.76/4.12 % copying label goal to answer in negative clause % 3.76/4.12 % 3.76/4.12 Term ordering decisions: % 3.76/4.12 Function symbol KB weights: bfalse=1. btrue=1. skip=1. fF=1. tT=1. zero=1. l=1. nil=1. h=1. eq4=1. eq3=1. assign=1. seq=1. while=1. nand=1. run=1. eq2=1. eval=1. eq=1. elem=1. andb=1. cons=1. del=1. eq5=1. orb=1. impl=1. prop=1. typeCorrect=1. var=1. secret=1. high=1. low=1. notb=1. suc=1. ifThenElse=1. aux=1. aux2=1. aux3=1. % 3.76/4.12 % 3.76/4.12 ============================== end of process initial clauses ======== % 3.76/4.12 % 3.76/4.12 ============================== CLAUSES FOR SEARCH ==================== % 3.76/4.12 % 3.76/4.12 ============================== end of clauses for search ============= % 3.76/4.12 % 3.76/4.12 ============================== SEARCH ================================ % 3.76/4.12 % 3.76/4.12 % Starting search at 0.02 seconds. % 3.76/4.12 % 3.76/4.12 NOTE: Back_subsumption disabled, ratio of kept to back_subsumed is 73 (0.00 of 0.32 sec). % 3.76/4.12 % 3.76/4.12 Low Water (keep): wt=49.000, iters=3389 % 3.76/4.12 % 3.76/4.12 Low Water (keep): wt=48.000, iters=3350 % 3.76/4.12 % 3.76/4.12 Low Water (keep): wt=46.000, iters=3397 % 3.76/4.12 % 3.76/4.12 Low Water (keep): wt=43.000, iters=3451 % 3.76/4.12 % 3.76/4.12 Low Water (keep): wt=41.000, iters=3372 % 3.76/4.12 % 3.76/4.12 Low Water (keep): wt=39.000, iters=3340 % 3.76/4.12 % 3.76/4.12 Low Water (keep): wt=37.000, iters=3343 % 3.76/4.12 % 3.76/4.12 Low Water (keep): wt=36.000, iters=3341 % 3.76/4.12 % 3.76/4.12 Low Water (keep): wt=34.000, iters=3357 % 3.76/4.12 % 3.76/4.12 Low Water (keep): wt=24.000, iters=3465 % 3.76/4.12 % 3.76/4.12 Low Water (keep): wt=23.000, iters=3494 % 3.76/4.12 % 3.76/4.12 Low Water (keep): wt=22.000, iters=3664 % 3.76/4.12 % 3.76/4.12 Low Water (displace): id=5146, wt=53.000 % 3.76/4.12 % 3.76/4.12 Low Water (displace): id=5854, wt=51.000 % 3.76/4.12 % 3.76/4.12 Low Water (displace): id=5145, wt=50.000 % 3.76/4.12 % 3.76/4.12 Low Water (displace): id=5855, wt=49.000 % 3.76/4.12 % 3.76/4.12 Low Water (displace): id=5654, wt=48.000 % 3.76/4.12 % 3.76/4.12 Low Water (displace): id=6777, wt=47.000 % 3.76/4.12 % 3.76/4.12 Low Water (displace): id=6769, wt=46.000 % 3.76/4.12 % 3.76/4.12 Low Water (displace): id=6765, wt=45.000 % 3.76/4.12 % 3.76/4.12 Low Water (displace): id=4352, wt=39.000 % 12.12/12.41 % 12.12/12.41 Low Water (displace): id=9051, wt=38.000 % 12.12/12.41 % 12.12/12.41 Low Water (displace): id=5758, wt=37.000 % 12.12/12.41 % 12.12/12.41 Low Water (displace): id=9237, wt=36.000 % 12.12/12.41 % 12.12/12.41 Low Water (displace): id=9361, wt=35.000 % 12.12/12.41 % 12.12/12.41 Low Water (displace): id=9358, wt=34.000 % 12.12/12.41 % 12.12/12.41 Low Water (keep): wt=21.000, iters=3333 % 12.12/12.41 % 12.12/12.41 Low Water (displace): id=10059, wt=33.000 % 12.12/12.41 % 12.12/12.41 Low Water (displace): id=10327, wt=32.000 % 12.12/12.41 % 12.12/12.41 Low Water (displace): id=10583, wt=31.000 % 12.12/12.41 % 12.12/12.41 Low Water (displace): id=10547, wt=30.000 % 12.12/12.41 % 12.12/12.41 Low Water (displace): id=10084, wt=29.000 % 12.12/12.41 % 12.12/12.41 Low Water (displace): id=14740, wt=20.000 % 12.12/12.41 % 12.12/12.41 ============================== PROOF ================================= % 12.12/12.41 % SZS status Unsatisfiable % 12.12/12.41 % SZS output start Refutation % 12.12/12.41 % 12.12/12.41 % Proof 1 at 10.97 (+ 0.45) seconds: goal. % 12.12/12.41 % Length of proof is 67. % 12.12/12.41 % Level of proof is 10. % 12.12/12.41 % Maximum clause weight is 30.000. % 12.12/12.41 % Given clauses 4086. % 12.12/12.41 % 12.12/12.41 2 secret(fF) = bfalse # label(axiom_012) # label(axiom). [assumption]. % 12.12/12.41 4 notb(bfalse) = btrue # label(axiom_014) # label(axiom). [assumption]. % 12.12/12.41 5 l = low(zero) # label(axiom_015) # label(axiom). [assumption]. % 12.12/12.41 6 low(zero) = l. [copy(5),flip(a)]. % 12.12/12.41 7 h = high(zero) # label(axiom_018) # label(axiom). [assumption]. % 12.12/12.41 8 high(zero) = h. [copy(7),flip(a)]. % 12.12/12.41 9 typeCorrect(skip) = btrue # label(axiom_034) # label(axiom). [assumption]. % 12.12/12.41 10 orb(btrue,A) = btrue # label(axiom_006) # label(axiom). [assumption]. % 12.12/12.41 11 orb(bfalse,A) = A # label(axiom_007) # label(axiom). [assumption]. % 12.12/12.41 12 impl(btrue,A) = A # label(axiom_016) # label(axiom). [assumption]. % 12.12/12.41 14 elem(A,nil) = bfalse # label(axiom_019) # label(axiom). [assumption]. % 12.12/12.41 15 del(A,nil) = nil # label(axiom_021) # label(axiom). [assumption]. % 12.12/12.41 16 andb(btrue,A) = A # label(axiom_023) # label(axiom). [assumption]. % 12.12/12.41 19 eval(A,fF) = bfalse # label(axiom_027) # label(axiom). [assumption]. % 12.12/12.41 20 run(A,skip) = A # label(axiom_029) # label(axiom). [assumption]. % 12.12/12.41 23 eq5(bfalse,btrue) = bfalse # label(axiom_043) # label(axiom). [assumption]. % 12.12/12.41 27 eq3(A,A) = btrue # label(axiom_096) # label(axiom). [assumption]. % 12.12/12.41 29 eq5(A,A) = btrue # label(axiom_098) # label(axiom). [assumption]. % 12.12/12.41 44 eq2(high(A),low(B)) = bfalse # label(axiom_060) # label(axiom). [assumption]. % 12.12/12.41 45 eq2(low(A),high(B)) = bfalse # label(axiom_061) # label(axiom). [assumption]. % 12.12/12.41 52 eval(A,var(B)) = elem(B,A) # label(axiom_028) # label(axiom). [assumption]. % 12.12/12.41 53 elem(A,B) = eval(B,var(A)). [copy(52),flip(a)]. % 12.12/12.41 58 aux(A,B,C,btrue) = del(A,C) # label(axiom) # label(axiom). [assumption]. % 12.12/12.41 60 aux2(A,B,C,bfalse) = del(B,A) # label(axiom_003) # label(axiom). [assumption]. % 12.12/12.41 61 typeCorrect(assign(low(A),B)) = notb(secret(B)) # label(axiom_036) # label(axiom). [assumption]. % 12.12/12.41 62 eq3(var(A),var(B)) = eq2(A,B) # label(axiom_047) # label(axiom). [assumption]. % 12.12/12.41 63 eq2(A,B) = eq3(var(A),var(B)). [copy(62),flip(a)]. % 12.12/12.41 76 aux3(A,B,C,D,btrue) = run(A,C) # label(axiom_004) # label(axiom). [assumption]. % 12.12/12.41 77 aux3(A,B,C,D,bfalse) = run(A,D) # label(axiom_005) # label(axiom). [assumption]. % 12.12/12.41 80 typeCorrect(seq(A,B)) = andb(typeCorrect(A),typeCorrect(B)) # label(axiom_037) # label(axiom). [assumption]. % 12.12/12.41 81 andb(typeCorrect(A),typeCorrect(B)) = typeCorrect(seq(A,B)). [copy(80),flip(a)]. % 12.12/12.41 91 typeCorrect(ifThenElse(A,B,C)) = andb(typeCorrect(B),typeCorrect(C)) # label(axiom_038) # label(axiom). [assumption]. % 12.12/12.41 92 typeCorrect(ifThenElse(A,B,C)) = typeCorrect(seq(B,C)). [copy(91),rewrite([81(5)])]. % 12.12/12.41 93 elem(A,cons(B,C)) = orb(eq2(B,A),elem(A,C)) # label(axiom_020) # label(axiom). [assumption]. % 12.12/12.41 94 orb(eq3(var(A),var(B)),eval(C,var(B))) = eval(cons(A,C),var(B)). [copy(93),rewrite([53(2),63(4),53(7)]),flip(a)]. % 12.12/12.41 95 del(A,cons(B,C)) = aux(A,B,C,eq2(A,B)) # label(axiom_022) # label(axiom). [assumption]. % 12.12/12.41 96 aux(A,B,C,eq3(var(A),var(B))) = del(A,cons(B,C)). [copy(95),rewrite([63(3)]),flip(a)]. % 12.12/12.41 97 run(A,assign(B,C)) = aux2(A,B,C,eval(A,C)) # label(axiom_030) # label(axiom). [assumption]. % 12.12/12.41 98 aux2(A,B,C,eval(A,C)) = run(A,assign(B,C)). [copy(97),flip(a)]. % 12.12/12.41 101 run(A,ifThenElse(B,C,D)) = aux3(A,B,C,D,eval(A,B)) # label(axiom_032) # label(axiom). [assumption]. % 12.12/12.41 102 aux3(A,B,C,D,eval(A,B)) = run(A,ifThenElse(B,C,D)). [copy(101),flip(a)]. % 12.12/12.41 105 prop(A,B) = impl(typeCorrect(A),eq5(elem(l,run(B,A)),elem(l,run(cons(h,B),A)))) # label(axiom_040) # label(axiom). [assumption]. % 12.12/12.41 106 prop(A,B) = impl(typeCorrect(A),eq5(eval(run(B,A),var(l)),eval(run(cons(h,B),A),var(l)))). [copy(105),rewrite([53(5),53(11)])]. % 12.12/12.41 107 eq5(prop(A,B),bfalse) != btrue # label(goal) # label(negated_conjecture) # answer(goal). [assumption]. % 12.12/12.41 108 eq5(impl(typeCorrect(A),eq5(eval(run(B,A),var(l)),eval(run(cons(h,B),A),var(l)))),bfalse) != btrue # answer(goal). [copy(107),rewrite([106(1)])]. % 12.12/12.41 122 eval(nil,var(A)) = bfalse. [back_rewrite(14),rewrite([53(2)])]. % 12.12/12.41 123 eq3(var(low(A)),var(high(B))) = bfalse. [back_rewrite(45),rewrite([63(3)])]. % 12.12/12.41 124 eq3(var(high(A)),var(low(B))) = bfalse. [back_rewrite(44),rewrite([63(3)])]. % 12.12/12.41 130 typeCorrect(assign(l,A)) = notb(secret(A)). [para(6(a,1),61(a,1,1,1))]. % 12.12/12.41 142 typeCorrect(seq(skip,A)) = typeCorrect(A). [para(9(a,1),81(a,1,1)),rewrite([16(3)]),flip(a)]. % 12.12/12.41 155 eval(cons(A,B),var(A)) = btrue. [para(27(a,1),94(a,1,1)),rewrite([10(4)]),flip(a)]. % 12.12/12.41 158 del(A,cons(A,B)) = del(A,B). [para(27(a,1),96(a,1,4)),rewrite([58(2)]),flip(a)]. % 12.12/12.41 162 run(A,assign(B,fF)) = del(B,A). [para(19(a,1),98(a,1,4)),rewrite([60(3)]),flip(a)]. % 12.12/12.41 176 eq5(impl(typeCorrect(seq(A,B)),eq5(eval(run(C,ifThenElse(D,A,B)),var(l)),eval(run(cons(h,C),ifThenElse(D,A,B)),var(l)))),bfalse) != btrue # answer(goal). [para(92(a,1),108(a,1,1,1))]. % 12.12/12.41 335 eq3(var(l),var(high(A))) = bfalse. [para(6(a,1),123(a,1,1,1))]. % 12.12/12.41 343 eq3(var(high(A)),var(l)) = bfalse. [para(6(a,1),124(a,1,2,1))]. % 12.12/12.41 415 eval(cons(A,cons(B,C)),var(B)) = orb(eq3(var(A),var(B)),btrue). [para(155(a,1),94(a,1,2)),flip(a)]. % 12.12/12.41 419 run(cons(A,B),ifThenElse(var(A),C,D)) = run(cons(A,B),C). [para(155(a,1),102(a,1,5)),rewrite([76(4)]),flip(a)]. % 12.12/12.41 434 eq3(var(l),var(h)) = bfalse. [para(8(a,1),335(a,1,2,1))]. % 12.12/12.41 452 eval(cons(l,A),var(h)) = eval(A,var(h)). [para(434(a,1),94(a,1,1)),rewrite([11(5)]),flip(a)]. % 12.12/12.41 464 eq3(var(h),var(l)) = bfalse. [para(8(a,1),343(a,1,1,1))]. % 12.12/12.41 1003 aux3(cons(l,A),var(h),B,C,eval(A,var(h))) = run(cons(l,A),ifThenElse(var(h),B,C)). [para(452(a,1),102(a,1,5))]. % 12.12/12.41 1069 eq5(impl(typeCorrect(A),eq5(eval(run(B,ifThenElse(C,skip,A)),var(l)),eval(run(cons(h,B),ifThenElse(C,skip,A)),var(l)))),bfalse) != btrue # answer(goal). [para(142(a,1),176(a,1,1,1))]. % 12.12/12.41 14615 run(cons(l,nil),ifThenElse(var(h),A,B)) = run(cons(l,nil),B). [para(122(a,1),1003(a,1,5)),rewrite([77(7)]),flip(a)]. % 12.12/12.41 14890 eq5(impl(typeCorrect(A),eq5(eval(run(cons(l,nil),A),var(l)),btrue)),bfalse) != btrue # answer(goal). [para(14615(a,1),1069(a,1,1,2,1,1)),rewrite([419(18),20(15),415(16),464(13),11(11)])]. % 12.12/12.41 14897 eq5(impl(typeCorrect(assign(A,fF)),eq5(eval(del(A,cons(l,nil)),var(l)),btrue)),bfalse) != btrue # answer(goal). [para(162(a,1),14890(a,1,1,2,1,1))]. % 12.12/12.41 16332 $F # answer(goal). [para(130(a,1),14897(a,1,1,1)),rewrite([2(2),4(2),158(6),15(4),122(5),23(4),12(3),29(3)]),xx(a)]. % 12.12/12.41 % 12.12/12.41 % SZS output end Refutation % 12.12/12.41 ============================== end of proof ========================== % 12.12/12.41 % 12.12/12.41 ============================== STATISTICS ============================ % 12.12/12.41 % 12.12/12.41 Given=4086. Generated=744485. Kept=16310. proofs=1. % 12.12/12.41 Usable=4034. Sos=9743. Demods=5785. Limbo=1, Disabled=2632. Hints=0. % 12.12/12.41 Megabytes=20.09. % 12.12/12.41 User_CPU=10.97, System_CPU=0.45, Wall_clock=12. % 12.12/12.41 % 12.12/12.41 ============================== end of statistics ===================== % 12.12/12.41 % 12.12/12.41 ============================== end of search ========================= % 12.12/12.41 % 12.12/12.41 THEOREM PROVED % 12.12/12.41 % SZS status Unsatisfiable % 12.12/12.41 % 12.12/12.41 Exiting with 1 proof. % 12.12/12.41 % 12.12/12.41 Process 24907 exit (max_proofs) Wed Apr 29 03:09:03 2026 % 12.12/12.41 Prover9 interrupted %------------------------------------------------------------------------------