%------------------------------------------------------------------------------ % File : CSE-F---1.0 % Problem : SYO631-1 : TPTP v7.5.0. Released v7.1.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n011.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 : 600s % DateTime : Tue Mar 29 01:05:44 EDT 2022 % Result : Unsatisfiable 186.24s 186.43s % Output : CNFRefutation 186.49s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SYO631-1 : TPTP v7.5.0. Released v7.1.0. % 0.03/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n011.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPUModel : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % RAMPerCPU : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 600 % 0.12/0.33 % DateTime : Mon Mar 14 09:58:42 EDT 2022 % 0.12/0.33 % CPUTime : % 0.19/0.44 openjdk version "1.8.0_171" % 0.19/0.44 OpenJDK Runtime Environment (build 1.8.0_171-b10) % 0.19/0.44 OpenJDK 64-Bit Server VM (build 25.171-b10, mixed mode) % 0.19/0.44 file=/export/starexec/sandbox2/benchmark/theBenchmark.p % 0.55/0.70 start to proof:theBenchmark % 186.24/186.43 % Version : CSE-F---1.0 % 186.24/186.43 % Problem : theBenchmark.p % 186.24/186.43 % Proof found % 186.24/186.43 % SZS status Theorem for theBenchmark.p % 186.24/186.43 % SZS output start Proof % 186.24/186.43 [11]P1(x111,x111) % 186.24/186.43 [22]P1(x221,f1(x221)) % 186.24/186.43 [23]~P2(f2(x231),a3) % 186.24/186.43 [35]~P3(f2(x351),f2(f1(x351))) % 186.24/186.43 [55]P2(f2(x551),f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(a3)))))))))))+P3(f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(a3)))))))))),f2(x551)) % 186.24/186.43 [37]P3(f2(x371),f2(f1(x371)))+~P3(a3,f2(x371))+~P3(a3,f2(f1(x371))) % 186.24/186.43 [39]~P3(f4(a3),f2(x391))+P3(f2(x391),f2(f1(x391)))+~P3(f4(a3),f2(f1(x391))) % 186.24/186.43 [40]P3(f2(x401),f2(f1(x401)))+~P3(f4(f4(a3)),f2(f1(x401)))+~P3(f4(f4(a3)),f2(x401)) % 186.24/186.43 [42]P3(f2(x421),f2(f1(x421)))+~P3(f4(f4(f4(a3))),f2(f1(x421)))+~P3(f4(f4(f4(a3))),f2(x421)) % 186.24/186.43 [44]P3(f2(x441),f2(f1(x441)))+~P3(f4(f4(f4(f4(a3)))),f2(f1(x441)))+~P3(f4(f4(f4(f4(a3)))),f2(x441)) % 186.24/186.43 [46]P3(f2(x461),f2(f1(x461)))+~P3(f4(f4(f4(f4(f4(a3))))),f2(f1(x461)))+~P3(f4(f4(f4(f4(f4(a3))))),f2(x461)) % 186.24/186.43 [48]P3(f2(x481),f2(f1(x481)))+~P3(f4(f4(f4(f4(f4(f4(a3)))))),f2(f1(x481)))+~P3(f4(f4(f4(f4(f4(f4(a3)))))),f2(x481)) % 186.24/186.43 [50]P3(f2(x501),f2(f1(x501)))+~P3(f4(f4(f4(f4(f4(f4(f4(a3))))))),f2(f1(x501)))+~P3(f4(f4(f4(f4(f4(f4(f4(a3))))))),f2(x501)) % 186.24/186.43 [52]P3(f2(x521),f2(f1(x521)))+~P3(f4(f4(f4(f4(f4(f4(f4(f4(a3)))))))),f2(f1(x521)))+~P3(f4(f4(f4(f4(f4(f4(f4(f4(a3)))))))),f2(x521)) % 186.24/186.43 [54]P3(f2(x541),f2(f1(x541)))+~P3(f4(f4(f4(f4(f4(f4(f4(f4(f4(a3))))))))),f2(f1(x541)))+~P3(f4(f4(f4(f4(f4(f4(f4(f4(f4(a3))))))))),f2(x541)) % 186.24/186.43 [57]P3(f2(x571),f2(f1(x571)))+~P3(f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(a3)))))))))),f2(f1(x571)))+~P3(f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(a3)))))))))),f2(x571)) % 186.24/186.43 [36]~P1(x362,x361)+~P2(f2(x362),f4(a3))+P3(a3,f2(x361))+P2(f2(x361),a3) % 186.24/186.43 [38]~P1(x382,x381)+P2(f2(x381),f4(a3))+P3(f4(a3),f2(x381))+~P2(f2(x382),f4(f4(a3))) % 186.24/186.43 [41]~P1(x412,x411)+P2(f2(x411),f4(f4(a3)))+P3(f4(f4(a3)),f2(x411))+~P2(f2(x412),f4(f4(f4(a3)))) % 186.24/186.43 [43]~P1(x432,x431)+P2(f2(x431),f4(f4(f4(a3))))+P3(f4(f4(f4(a3))),f2(x431))+~P2(f2(x432),f4(f4(f4(f4(a3))))) % 186.24/186.43 [45]~P1(x452,x451)+P2(f2(x451),f4(f4(f4(f4(a3)))))+P3(f4(f4(f4(f4(a3)))),f2(x451))+~P2(f2(x452),f4(f4(f4(f4(f4(a3)))))) % 186.24/186.43 [47]~P1(x472,x471)+P2(f2(x471),f4(f4(f4(f4(f4(a3))))))+P3(f4(f4(f4(f4(f4(a3))))),f2(x471))+~P2(f2(x472),f4(f4(f4(f4(f4(f4(a3))))))) % 186.24/186.43 [49]~P1(x492,x491)+P2(f2(x491),f4(f4(f4(f4(f4(f4(a3)))))))+P3(f4(f4(f4(f4(f4(f4(a3)))))),f2(x491))+~P2(f2(x492),f4(f4(f4(f4(f4(f4(f4(a3)))))))) % 186.24/186.43 [51]~P1(x512,x511)+P2(f2(x511),f4(f4(f4(f4(f4(f4(f4(a3))))))))+P3(f4(f4(f4(f4(f4(f4(f4(a3))))))),f2(x511))+~P2(f2(x512),f4(f4(f4(f4(f4(f4(f4(f4(a3))))))))) % 186.24/186.43 [53]~P1(x532,x531)+P2(f2(x531),f4(f4(f4(f4(f4(f4(f4(f4(a3)))))))))+P3(f4(f4(f4(f4(f4(f4(f4(f4(a3)))))))),f2(x531))+~P2(f2(x532),f4(f4(f4(f4(f4(f4(f4(f4(f4(a3)))))))))) % 186.24/186.43 [56]~P1(x562,x561)+P2(f2(x561),f4(f4(f4(f4(f4(f4(f4(f4(f4(a3))))))))))+P3(f4(f4(f4(f4(f4(f4(f4(f4(f4(a3))))))))),f2(x561))+~P2(f2(x562),f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(a3))))))))))) % 186.33/186.53 cnf(58,plain, % 186.33/186.53 (P2(f2(f1(x581)),f4(f4(f4(f4(f4(f4(f4(f4(f4(a3))))))))))+P3(f4(f4(f4(f4(f4(f4(f4(f4(f4(a3))))))))),f2(f1(x581)))+P3(f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(a3)))))))))),f2(x581))), % 186.33/186.53 inference(scs_inference,[],[22,55,56])). % 186.33/186.53 cnf(59,plain, % 186.33/186.53 (~P2(f2(x591),f4(a3))+~P3(a3,f2(f1(x591)))), % 186.33/186.53 inference(scs_inference,[],[35,23,11,37,36])). % 186.33/186.53 cnf(60,plain, % 186.33/186.53 (~P3(a3,f2(f1(x601)))+P3(f4(a3),f2(x601))+~P2(f2(x601),f4(f4(a3)))), % 186.33/186.53 inference(scs_inference,[],[11,59,38])). % 186.33/186.53 cnf(61,plain, % 186.33/186.53 (~P2(f2(x611),f4(f4(a3)))+~P3(a3,f2(f1(x611)))+~P3(f4(a3),f2(f1(x611)))), % 186.33/186.53 inference(scs_inference,[],[35,39,60])). % 186.33/186.53 cnf(62,plain, % 186.33/186.53 (P2(f2(f1(x621)),f4(f4(a3)))+~P3(f4(f4(a3)),f2(x621))+~P2(f2(x621),f4(f4(f4(a3))))), % 186.33/186.53 inference(scs_inference,[],[35,22,40,41])). % 186.33/186.53 cnf(63,plain, % 186.33/186.53 (P2(f2(f1(x631)),f4(f4(f4(a3))))+~P3(f4(f4(f4(a3))),f2(x631))+~P2(f2(x631),f4(f4(f4(f4(a3)))))), % 186.33/186.53 inference(scs_inference,[],[35,22,42,43])). % 186.33/186.53 cnf(64,plain, % 186.33/186.53 (P2(f2(f1(x641)),f4(f4(f4(f4(a3)))))+~P3(f4(f4(f4(f4(a3)))),f2(x641))+~P2(f2(f1(x641)),f4(f4(f4(f4(f4(a3))))))), % 186.33/186.53 inference(scs_inference,[],[35,11,44,45])). % 186.33/186.53 cnf(66,plain, % 186.33/186.53 (P2(f2(f1(x661)),f4(f4(f4(f4(f4(f4(a3)))))))+~P3(f4(f4(f4(f4(f4(f4(a3)))))),f2(x661))+~P2(f2(x661),f4(f4(f4(f4(f4(f4(f4(a3))))))))), % 186.33/186.53 inference(scs_inference,[],[35,22,48,49])). % 186.33/186.53 cnf(68,plain, % 186.33/186.53 (P2(f2(f1(x681)),f4(f4(f4(f4(f4(f4(f4(f4(a3)))))))))+~P3(f4(f4(f4(f4(f4(f4(f4(f4(a3)))))))),f2(x681))+~P2(f2(x681),f4(f4(f4(f4(f4(f4(f4(f4(f4(a3))))))))))), % 186.33/186.53 inference(scs_inference,[],[35,22,52,53])). % 186.33/186.53 cnf(69,plain, % 186.33/186.53 (P3(f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(a3)))))))))),f2(x691))+P2(f2(f1(x691)),f4(f4(f4(f4(f4(f4(f4(f4(f4(a3))))))))))+~P3(f4(f4(f4(f4(f4(f4(f4(f4(f4(a3))))))))),f2(x691))), % 186.33/186.53 inference(scs_inference,[],[35,54,58])). % 186.33/186.53 cnf(70,plain, % 186.33/186.53 (~P3(f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(a3)))))))))),f2(x701))+P2(f2(f1(x701)),f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(a3)))))))))))), % 186.33/186.53 inference(scs_inference,[],[35,57,55])). % 186.33/186.53 cnf(77,plain, % 186.33/186.53 (P2(f2(f1(x771)),f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(a3)))))))))))+P2(f2(x771),f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(a3)))))))))))), % 186.33/186.53 inference(scs_inference,[],[70,55])). % 186.33/186.53 cnf(79,plain, % 186.33/186.53 (P2(f2(f1(x791)),f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(a3)))))))))))+P2(f2(f1(x791)),f4(f4(f4(f4(f4(f4(f4(f4(f4(a3))))))))))+P3(f4(f4(f4(f4(f4(f4(f4(f4(f4(a3))))))))),f2(f1(x791)))), % 186.33/186.53 inference(scs_inference,[],[70,58])). % 186.33/186.53 cnf(80,plain, % 186.33/186.53 (P2(f2(f1(x801)),f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(a3)))))))))))+P2(f2(f1(x801)),f4(f4(f4(f4(f4(f4(f4(f4(f4(a3))))))))))+~P3(f4(f4(f4(f4(f4(f4(f4(f4(f4(a3))))))))),f2(x801))), % 186.33/186.53 inference(scs_inference,[],[70,69])). % 186.33/186.53 cnf(81,plain, % 186.33/186.53 (P2(f2(x811),f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(a3)))))))))))+P2(f2(f1(f1(x811))),f4(f4(f4(f4(f4(f4(f4(f4(f4(a3))))))))))+P3(f4(f4(f4(f4(f4(f4(f4(f4(f4(a3))))))))),f2(f1(f1(x811))))), % 186.33/186.53 inference(scs_inference,[],[22,77,56])). % 186.33/186.53 cnf(82,plain, % 186.33/186.53 (~P2(f2(x821),f4(a3))+~P3(a3,f2(x821))), % 186.33/186.53 inference(scs_inference,[],[35,23,22,37,36])). % 186.33/186.53 cnf(85,plain, % 186.33/186.53 (~P3(a3,f2(f1(x851)))+P3(f4(a3),f2(f1(x851)))+~P2(f2(x851),f4(f4(a3)))), % 186.33/186.53 inference(scs_inference,[],[22,82,38])). % 186.33/186.53 cnf(86,plain, % 186.33/186.53 (~P2(f2(x861),f4(f4(a3)))+~P3(a3,f2(f1(x861)))), % 186.33/186.53 inference(scs_inference,[],[85,61])). % 186.33/186.53 cnf(88,plain, % 186.33/186.53 (~P2(f2(x881),f4(f4(a3)))+~P2(f2(f1(x881)),f4(a3))), % 186.33/186.53 inference(scs_inference,[],[23,11,86,36])). % 186.33/186.53 cnf(92,plain, % 186.33/186.53 (~P2(f2(x921),f4(f4(a3)))+~P2(f2(x921),f4(a3))), % 186.33/186.53 inference(scs_inference,[],[23,22,86,36])). % 186.33/186.53 cnf(97,plain, % 186.33/186.53 (~P2(f2(x971),f4(f4(a3)))+P3(f4(a3),f2(x971))), % 186.33/186.53 inference(scs_inference,[],[11,92,38])). % 186.33/186.53 cnf(99,plain, % 186.33/186.53 (~P2(f2(x991),f4(f4(a3)))+~P3(f4(a3),f2(f1(x991)))), % 186.33/186.53 inference(scs_inference,[],[35,97,39])). % 186.33/186.53 cnf(100,plain, % 186.33/186.53 (~P2(f2(x1001),f4(f4(f4(a3))))+~P3(f4(f4(a3)),f2(x1001))+~P3(f4(a3),f2(f1(f1(x1001))))), % 186.33/186.53 inference(scs_inference,[],[99,62])). % 186.33/186.53 cnf(111,plain, % 186.33/186.53 (~P2(f2(x1111),f4(f4(a3)))+P3(f4(a3),f2(f1(x1111)))), % 186.33/186.53 inference(scs_inference,[],[22,88,38])). % 186.33/186.53 cnf(112,plain, % 186.33/186.53 (~P2(f2(x1121),f4(f4(f4(a3))))+~P3(f4(f4(a3)),f2(x1121))+P3(f4(a3),f2(f1(f1(x1121))))), % 186.33/186.53 inference(scs_inference,[],[111,62])). % 186.33/186.53 cnf(113,plain, % 186.33/186.53 (~P2(f2(x1131),f4(f4(f4(a3))))+~P3(f4(f4(a3)),f2(x1131))), % 186.33/186.53 inference(scs_inference,[],[112,100])). % 186.33/186.53 cnf(122,plain, % 186.33/186.53 (~P2(f2(x1221),f4(f4(a3)))), % 186.33/186.53 inference(scs_inference,[],[99,111])). % 186.33/186.53 cnf(64315,plain, % 186.33/186.53 (~P3(f4(f4(f4(f4(a3)))),f2(f1(x643151)))+~P3(f4(f4(f4(f4(a3)))),f2(x643151))), % 186.33/186.53 inference(scs_inference,[],[22,122,35,41,44])). % 186.33/186.53 cnf(64317,plain, % 186.33/186.53 (~P3(f4(f4(f4(f4(f4(a3))))),f2(f1(x643171)))+~P3(f4(f4(f4(f4(f4(a3))))),f2(x643171))), % 186.33/186.53 inference(scs_inference,[],[35,46])). % 186.33/186.53 cnf(64319,plain, % 186.33/186.53 (~P3(f4(f4(f4(f4(f4(f4(a3)))))),f2(f1(x643191)))+~P3(f4(f4(f4(f4(f4(f4(a3)))))),f2(x643191))), % 186.33/186.53 inference(scs_inference,[],[35,46,48])). % 186.33/186.53 cnf(64321,plain, % 186.33/186.53 (~P3(f4(f4(f4(f4(f4(f4(f4(a3))))))),f2(f1(x643211)))+~P3(f4(f4(f4(f4(f4(f4(f4(a3))))))),f2(x643211))), % 186.33/186.53 inference(scs_inference,[],[35,50])). % 186.33/186.53 cnf(64323,plain, % 186.33/186.53 (~P3(f4(f4(f4(f4(f4(f4(f4(f4(a3)))))))),f2(f1(x643231)))+~P3(f4(f4(f4(f4(f4(f4(f4(f4(a3)))))))),f2(x643231))), % 186.33/186.53 inference(scs_inference,[],[35,52])). % 186.33/186.53 cnf(64325,plain, % 186.33/186.53 (P3(f4(f4(f4(a3))),f2(f1(x643251)))+P2(f2(f1(x643251)),f4(f4(f4(a3))))+~P2(f2(x643251),f4(f4(f4(f4(a3)))))), % 186.33/186.53 inference(scs_inference,[],[22,35,43])). % 186.33/186.53 cnf(64326,plain, % 186.33/186.53 (~P3(f4(f4(f4(f4(f4(f4(f4(f4(f4(a3))))))))),f2(f1(x643261)))+~P3(f4(f4(f4(f4(f4(f4(f4(f4(f4(a3))))))))),f2(x643261))), % 186.33/186.53 inference(scs_inference,[],[35,54])). % 186.33/186.53 cnf(64337,plain, % 186.33/186.53 (P2(f2(x643371),f4(f4(f4(a3))))+P3(f4(f4(f4(a3))),f2(x643371))+~P2(f2(x643371),f4(f4(f4(f4(a3)))))), % 186.33/186.53 inference(scs_inference,[],[11,43])). % 186.33/186.53 cnf(64339,plain, % 186.33/186.53 (~P3(f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(a3)))))))))),f2(f1(x643391)))+~P3(f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(a3)))))))))),f2(x643391))), % 186.33/186.53 inference(scs_inference,[],[35,57])). % 186.33/186.53 cnf(64343,plain, % 186.33/186.53 (P3(f4(f4(f4(f4(a3)))),f2(x643431))+P2(f2(x643431),f4(f4(f4(f4(a3)))))+~P2(f2(x643431),f4(f4(f4(f4(f4(a3))))))), % 186.33/186.53 inference(scs_inference,[],[11,45])). % 186.33/186.53 cnf(64344,plain, % 186.33/186.53 (~P3(f4(f4(f4(f4(f4(a3))))),f2(f1(x643441)))+P2(f2(x643441),f4(f4(f4(f4(f4(a3))))))+~P2(f2(x643441),f4(f4(f4(f4(f4(f4(a3)))))))), % 186.33/186.53 inference(scs_inference,[],[11,64317,47])). % 186.33/186.53 cnf(64345,plain, % 186.33/186.53 (P2(f2(x643451),f4(f4(f4(f4(f4(f4(f4(f4(f4(a3))))))))))+P3(f4(f4(f4(f4(f4(f4(f4(f4(f4(a3))))))))),f2(x643451))+~P2(f2(x643451),f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(a3)))))))))))), % 186.33/186.53 inference(scs_inference,[],[11,56])). % 186.33/186.53 cnf(64347,plain, % 186.33/186.53 (~P3(f4(f4(f4(f4(f4(f4(a3)))))),f2(f1(x643471)))+P2(f2(x643471),f4(f4(f4(f4(f4(f4(a3)))))))+~P2(f2(x643471),f4(f4(f4(f4(f4(f4(f4(a3))))))))), % 186.33/186.53 inference(scs_inference,[],[11,64319,49])). % 186.33/186.53 cnf(64348,plain, % 186.33/186.53 (~P3(f4(f4(f4(f4(f4(f4(f4(a3))))))),f2(f1(x643481)))+P2(f2(x643481),f4(f4(f4(f4(f4(f4(f4(a3))))))))+~P2(f2(x643481),f4(f4(f4(f4(f4(f4(f4(f4(a3)))))))))), % 186.33/186.53 inference(scs_inference,[],[11,64321,51])). % 186.33/186.53 cnf(64349,plain, % 186.33/186.53 (~P3(f4(f4(f4(f4(f4(f4(f4(f4(a3)))))))),f2(f1(f1(x643491))))+P2(f2(f1(x643491)),f4(f4(f4(f4(f4(f4(f4(f4(a3)))))))))+~P2(f2(x643491),f4(f4(f4(f4(f4(f4(f4(f4(f4(a3))))))))))), % 186.33/186.53 inference(scs_inference,[],[22,64323,53])). % 186.33/186.53 cnf(64353,plain, % 186.33/186.53 (~P3(f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(a3)))))))))),f2(f1(x643531)))+P2(f2(x643531),f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(a3)))))))))))), % 186.33/186.53 inference(scs_inference,[],[64339,55])). % 186.33/186.53 cnf(64355,plain, % 186.33/186.53 (~P3(f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(a3)))))))))),f2(f1(x643551)))+P2(f2(x643551),f4(f4(f4(f4(f4(f4(f4(f4(f4(a3))))))))))+P3(f4(f4(f4(f4(f4(f4(f4(f4(f4(a3))))))))),f2(x643551))), % 186.33/186.53 inference(scs_inference,[],[64353,64345])). % 186.33/186.53 cnf(65227,plain, % 186.33/186.53 (P3(f4(f4(f4(f4(a3)))),f2(f1(x652271)))+P2(f2(f1(x652271)),f4(f4(f4(f4(a3)))))+~P2(f2(x652271),f4(f4(f4(f4(f4(a3))))))), % 186.33/186.53 inference(scs_inference,[],[22,45])). % 186.33/186.53 cnf(65229,plain, % 186.33/186.53 (P2(f2(x652291),f4(f4(f4(f4(f4(a3))))))+P3(f4(f4(f4(f4(f4(a3))))),f2(x652291))+~P2(f2(x652291),f4(f4(f4(f4(f4(f4(a3)))))))), % 186.33/186.53 inference(scs_inference,[],[11,47])). % 186.33/186.53 cnf(65231,plain, % 186.33/186.53 (P2(f2(f1(x652311)),f4(f4(f4(f4(f4(f4(a3)))))))+P3(f4(f4(f4(f4(f4(f4(a3)))))),f2(f1(x652311)))+~P2(f2(x652311),f4(f4(f4(f4(f4(f4(f4(a3))))))))), % 186.33/186.53 inference(scs_inference,[],[22,49])). % 186.33/186.53 cnf(65237,plain, % 186.33/186.53 (P2(f2(f1(x652371)),f4(f4(f4(f4(f4(a3))))))+P3(f4(f4(f4(f4(f4(a3))))),f2(f1(x652371)))+~P2(f2(x652371),f4(f4(f4(f4(f4(f4(a3)))))))), % 186.33/186.53 inference(scs_inference,[],[22,47])). % 186.33/186.53 cnf(65239,plain, % 186.33/186.53 (P3(f4(f4(f4(f4(f4(f4(f4(f4(a3)))))))),f2(x652391))+P2(f2(x652391),f4(f4(f4(f4(f4(f4(f4(f4(a3)))))))))+~P2(f2(x652391),f4(f4(f4(f4(f4(f4(f4(f4(f4(a3))))))))))), % 186.33/186.53 inference(scs_inference,[],[11,53])). % 186.33/186.53 cnf(65241,plain, % 186.33/186.53 (P3(f4(f4(f4(f4(f4(f4(f4(a3))))))),f2(f1(x652411)))+P2(f2(f1(x652411)),f4(f4(f4(f4(f4(f4(f4(a3))))))))+~P2(f2(x652411),f4(f4(f4(f4(f4(f4(f4(f4(a3)))))))))), % 186.33/186.53 inference(scs_inference,[],[22,51])). % 186.33/186.53 cnf(65249,plain, % 186.33/186.53 (P2(f2(f1(x652491)),f4(f4(f4(f4(f4(f4(f4(f4(a3)))))))))+P3(f4(f4(f4(f4(f4(f4(f4(f4(a3)))))))),f2(f1(x652491)))+~P2(f2(x652491),f4(f4(f4(f4(f4(f4(f4(f4(f4(a3))))))))))), % 186.33/186.53 inference(scs_inference,[],[22,53])). % 186.33/186.53 cnf(65255,plain, % 186.33/186.53 (P3(f4(f4(f4(f4(f4(f4(a3)))))),f2(x652551))+P2(f2(x652551),f4(f4(f4(f4(f4(f4(a3)))))))+P3(f4(f4(f4(f4(f4(f4(f4(a3))))))),f2(x652551))+~P2(f2(x652551),f4(f4(f4(f4(f4(f4(f4(f4(a3)))))))))), % 186.33/186.53 inference(scs_inference,[],[11,49,51])). % 186.33/186.53 cnf(65282,plain, % 186.33/186.53 (P2(f2(x652821),f4(f4(f4(f4(f4(f4(a3)))))))+P3(f4(f4(f4(f4(f4(f4(a3)))))),f2(x652821))+~P2(f2(x652821),f4(f4(f4(f4(f4(f4(f4(a3))))))))), % 186.33/186.53 inference(scs_inference,[],[11,49])). % 186.33/186.53 cnf(176961,plain, % 186.33/186.53 (~P2(f2(x1769611),f4(f4(f4(a3))))), % 186.33/186.53 inference(scs_inference,[],[11,122,41,113])). % 186.33/186.53 cnf(176964,plain, % 186.33/186.53 (~P2(f2(x1769641),f4(f4(f4(a3))))), % 186.33/186.53 inference(rename_variables,[],[176961])). % 186.33/186.54 cnf(176965,plain, % 186.33/186.54 (~P2(f2(x1769651),f4(f4(f4(a3))))), % 186.33/186.54 inference(rename_variables,[],[176961])). % 186.33/186.54 cnf(176966,plain, % 186.33/186.54 (~P2(f2(f1(x1769661)),f4(f4(f4(f4(a3)))))), % 186.33/186.54 inference(scs_inference,[],[176961,176964,176965,63,64325,64337])). % 186.33/186.54 cnf(177355,plain, % 186.33/186.54 (P3(f4(f4(f4(f4(a3)))),f2(f1(x1773551)))+~P2(f2(f1(x1773551)),f4(f4(f4(f4(f4(a3))))))), % 186.33/186.54 inference(scs_inference,[],[11,176961,176966,45])). % 186.33/186.54 cnf(177433,plain, % 186.33/186.54 (~P2(f2(f1(x1774331)),f4(f4(f4(f4(f4(a3))))))+P2(f2(f1(f1(x1774331))),f4(f4(f4(f4(a3)))))), % 186.33/186.54 inference(scs_inference,[],[176966,64343,64315,177355,64,65227])). % 186.33/186.54 cnf(177434,plain, % 186.33/186.54 (~P2(f2(f1(x1774341)),f4(f4(f4(f4(f4(a3))))))), % 186.33/186.54 inference(scs_inference,[],[176966,177433])). % 186.33/186.54 cnf(177519,plain, % 186.33/186.54 (~P2(f2(x1775191),f4(f4(f4(f4(f4(f4(a3)))))))+P3(f4(f4(f4(f4(f4(a3))))),f2(f1(x1775191)))), % 186.33/186.54 inference(scs_inference,[],[177434,65237])). % 186.33/186.54 cnf(177547,plain, % 186.33/186.54 (~P2(f2(f1(x1775471)),f4(f4(f4(f4(f4(f4(a3)))))))), % 186.33/186.54 inference(scs_inference,[],[177434,64344,177519])). % 186.33/186.54 cnf(177615,plain, % 186.33/186.54 (~P2(f2(f1(x1776151)),f4(f4(f4(f4(f4(a3))))))), % 186.33/186.54 inference(rename_variables,[],[177434])). % 186.33/186.54 cnf(177617,plain, % 186.33/186.54 (~P2(f2(f1(f1(x1776171))),f4(f4(f4(f4(f4(f4(f4(a3))))))))+~P2(f2(f1(x1776171)),f4(f4(f4(f4(f4(f4(f4(a3))))))))+P2(f2(f1(f1(x1776171))),f4(f4(f4(f4(f4(f4(a3)))))))), % 186.33/186.54 inference(scs_inference,[],[11,177547,177434,177615,66,65231,65282,65229,64344,49])). % 186.33/186.54 cnf(177763,plain, % 186.33/186.54 (~P2(f2(f1(x1777631)),f4(f4(f4(f4(f4(f4(a3)))))))), % 186.33/186.54 inference(rename_variables,[],[177547])). % 186.33/186.54 cnf(177764,plain, % 186.33/186.54 (~P2(f2(f1(x1777641)),f4(f4(f4(f4(f4(f4(f4(a3))))))))), % 186.33/186.54 inference(scs_inference,[],[177547,177763,65231,64319,177617,64347])). % 186.33/186.54 cnf(177855,plain, % 186.33/186.54 (~P2(f2(f1(x1778551)),f4(f4(f4(f4(f4(f4(a3)))))))), % 186.33/186.54 inference(rename_variables,[],[177547])). % 186.33/186.54 cnf(177856,plain, % 186.33/186.54 (~P2(f2(f1(x1778561)),f4(f4(f4(f4(f4(f4(a3)))))))), % 186.33/186.54 inference(rename_variables,[],[177547])). % 186.33/186.54 cnf(177857,plain, % 186.33/186.54 (~P2(f2(f1(x1778571)),f4(f4(f4(f4(f4(f4(a3)))))))), % 186.33/186.54 inference(rename_variables,[],[177547])). % 186.33/186.54 cnf(177858,plain, % 186.33/186.54 (~P2(f2(f1(x1778581)),f4(f4(f4(f4(f4(f4(a3)))))))), % 186.33/186.54 inference(rename_variables,[],[177547])). % 186.33/186.54 cnf(177861,plain, % 186.33/186.54 (~P2(f2(f1(x1778611)),f4(f4(f4(f4(f4(f4(f4(f4(a3)))))))))), % 186.33/186.54 inference(scs_inference,[],[11,177764,177547,177855,177856,177857,177858,64348,65241,66,65231,65282,65255,49])). % 186.33/186.54 cnf(178119,plain, % 186.33/186.54 (~P2(f2(f1(x1781191)),f4(f4(f4(f4(f4(f4(f4(f4(f4(a3))))))))))+P2(f2(f1(f1(f1(x1781191)))),f4(f4(f4(f4(f4(f4(f4(f4(a3)))))))))+P3(f4(f4(f4(f4(f4(f4(f4(f4(f4(a3))))))))),f2(f1(f1(x1781191))))+~P2(f2(f1(f1(x1781191))),f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(a3)))))))))))), % 186.33/186.54 inference(scs_inference,[],[11,177861,177434,177547,65249,64323,68,56])). % 186.33/186.54 cnf(178170,plain, % 186.33/186.54 (~P2(f2(f1(x1781701)),f4(f4(f4(f4(f4(f4(f4(f4(a3)))))))))), % 186.33/186.54 inference(rename_variables,[],[177861])). % 186.33/186.54 cnf(178171,plain, % 186.33/186.54 (~P2(f2(f1(f1(x1781711))),f4(f4(f4(f4(f4(f4(f4(f4(f4(a3))))))))))), % 186.33/186.54 inference(scs_inference,[],[11,177861,178170,177547,65249,64323,68,64349,65239,65231,178119,53])). % 186.33/186.54 cnf(178177,plain, % 186.33/186.54 (~P3(f4(f4(f4(f4(f4(f4(f4(f4(f4(f4(a3)))))))))),f2(f1(f1(f1(x1781771)))))+P3(f4(f4(f4(f4(f4(f4(f4(f4(f4(a3))))))))),f2(f1(f1(x1781771))))), % 186.33/186.54 inference(scs_inference,[],[178171,177764,64355])). % 186.33/186.54 cnf(178225,plain, % 186.33/186.54 (~P3(f4(f4(f4(f4(f4(f4(f4(f4(f4(a3))))))))),f2(f1(x1782251)))), % 186.33/186.54 inference(scs_inference,[],[11,178171,80,56,64326])). % 186.33/186.54 cnf(178233,plain, % 186.33/186.54 (~P3(f4(f4(f4(f4(f4(f4(f4(f4(f4(a3))))))))),f2(f1(x1782331)))), % 186.33/186.54 inference(rename_variables,[],[178225])). % 186.33/186.54 cnf(178235,plain, % 186.33/186.54 (~P3(f4(f4(f4(f4(f4(f4(f4(f4(f4(a3))))))))),f2(f1(x1782351)))), % 186.33/186.54 inference(rename_variables,[],[178225])). % 186.33/186.54 cnf(178238,plain, % 186.33/186.54 (~P3(f4(f4(f4(f4(f4(f4(f4(f4(f4(a3))))))))),f2(f1(x1782381)))), % 186.33/186.54 inference(rename_variables,[],[178225])). % 186.33/186.54 cnf(178240,plain, % 186.33/186.54 ($false), % 186.33/186.54 inference(scs_inference,[],[178225,178233,178235,178238,178171,178177,79,81,58]), % 186.33/186.54 ['proof']). % 186.49/186.64 % SZS output end Proof % 186.49/186.64 % Total time : 185.480000 s %------------------------------------------------------------------------------