%------------------------------------------------------------------------------ % File : CSE-F---1.0 % Problem : SYO630-1 : TPTP v7.5.0. Released v7.1.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %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 : 600s % DateTime : Tue Mar 29 01:05:44 EDT 2022 % Result : Unsatisfiable 1.26s 1.38s % Output : CNFRefutation 1.32s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.11 % Problem : SYO630-1 : TPTP v7.5.0. Released v7.1.0. % 0.11/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n010.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:50:06 EDT 2022 % 0.12/0.33 % CPUTime : % 0.18/0.44 openjdk version "1.8.0_171" % 0.18/0.44 OpenJDK Runtime Environment (build 1.8.0_171-b10) % 0.18/0.44 OpenJDK 64-Bit Server VM (build 25.171-b10, mixed mode) % 0.18/0.44 file=/export/starexec/sandbox/benchmark/theBenchmark.p % 0.51/0.63 start to proof:theBenchmark % 1.26/1.38 % Version : CSE-F---1.0 % 1.26/1.38 % Problem : theBenchmark.p % 1.26/1.38 % Proof found % 1.26/1.38 % SZS status Theorem for theBenchmark.p % 1.26/1.38 % SZS output start Proof % 1.26/1.38 [6]P1(x61,x61) % 1.26/1.38 [12]P1(x121,f1(x121)) % 1.26/1.38 [13]~P2(f2(x131),a3) % 1.26/1.38 [20]~P3(f2(x201),f2(f1(x201))) % 1.26/1.38 [29]P2(f2(x291),f4(f4(f4(f4(f4(a3))))))+P3(f4(f4(f4(f4(f4(a3))))),f2(x291)) % 1.26/1.38 [22]P3(f2(x221),f2(f1(x221)))+~P3(a3,f2(x221))+~P3(a3,f2(f1(x221))) % 1.26/1.38 [24]~P3(f4(a3),f2(x241))+P3(f2(x241),f2(f1(x241)))+~P3(f4(a3),f2(f1(x241))) % 1.26/1.38 [25]P3(f2(x251),f2(f1(x251)))+~P3(f4(f4(a3)),f2(f1(x251)))+~P3(f4(f4(a3)),f2(x251)) % 1.26/1.38 [27]P3(f2(x271),f2(f1(x271)))+~P3(f4(f4(f4(a3))),f2(f1(x271)))+~P3(f4(f4(f4(a3))),f2(x271)) % 1.26/1.38 [30]P3(f2(x301),f2(f1(x301)))+~P3(f4(f4(f4(f4(a3)))),f2(f1(x301)))+~P3(f4(f4(f4(f4(a3)))),f2(x301)) % 1.26/1.38 [32]P3(f2(x321),f2(f1(x321)))+~P3(f4(f4(f4(f4(f4(a3))))),f2(f1(x321)))+~P3(f4(f4(f4(f4(f4(a3))))),f2(x321)) % 1.26/1.38 [21]~P1(x212,x211)+~P2(f2(x212),f4(a3))+P3(a3,f2(x211))+P2(f2(x211),a3) % 1.26/1.38 [23]~P1(x232,x231)+P2(f2(x231),f4(a3))+P3(f4(a3),f2(x231))+~P2(f2(x232),f4(f4(a3))) % 1.26/1.38 [26]~P1(x262,x261)+P2(f2(x261),f4(f4(a3)))+P3(f4(f4(a3)),f2(x261))+~P2(f2(x262),f4(f4(f4(a3)))) % 1.26/1.38 [28]~P1(x282,x281)+P2(f2(x281),f4(f4(f4(a3))))+P3(f4(f4(f4(a3))),f2(x281))+~P2(f2(x282),f4(f4(f4(f4(a3))))) % 1.26/1.38 [31]~P1(x312,x311)+P2(f2(x311),f4(f4(f4(f4(a3)))))+P3(f4(f4(f4(f4(a3)))),f2(x311))+~P2(f2(x312),f4(f4(f4(f4(f4(a3)))))) % 1.32/1.39 cnf(34,plain, % 1.32/1.39 (~P2(f2(x341),f4(a3))+~P3(a3,f2(f1(x341)))), % 1.32/1.39 inference(scs_inference,[],[20,13,6,22,21])). % 1.32/1.39 cnf(37,plain, % 1.32/1.39 (P2(f2(f1(x371)),f4(f4(a3)))+~P3(f4(f4(a3)),f2(x371))+~P2(f2(x371),f4(f4(f4(a3))))), % 1.32/1.39 inference(scs_inference,[],[20,12,25,26])). % 1.32/1.39 cnf(38,plain, % 1.32/1.39 (P2(f2(f1(x381)),f4(f4(f4(a3))))+~P3(f4(f4(f4(a3))),f2(x381))+~P2(f2(x381),f4(f4(f4(f4(a3)))))), % 1.32/1.39 inference(scs_inference,[],[20,12,27,28])). % 1.32/1.39 cnf(45,plain, % 1.32/1.39 (~P2(f2(x451),f4(a3))+~P2(f2(f1(x451)),f4(a3))), % 1.32/1.39 inference(scs_inference,[],[13,6,34,21])). % 1.32/1.39 cnf(46,plain, % 1.32/1.39 (~P2(f2(x461),f4(a3))+P3(f4(a3),f2(f1(x461)))+~P2(f2(f1(x461)),f4(f4(a3)))), % 1.32/1.39 inference(scs_inference,[],[6,45,23])). % 1.32/1.39 cnf(48,plain, % 1.32/1.39 (~P2(f2(x481),f4(a3))+P3(f4(a3),f2(f1(x481)))+~P2(f2(x481),f4(f4(a3)))), % 1.32/1.39 inference(scs_inference,[],[12,45,23])). % 1.32/1.39 cnf(51,plain, % 1.32/1.39 (P2(f2(x511),f4(f4(f4(f4(a3)))))+P3(f4(f4(f4(f4(a3)))),f2(x511))+P3(f4(f4(f4(f4(f4(a3))))),f2(x511))), % 1.32/1.39 inference(scs_inference,[],[6,29,31])). % 1.32/1.39 cnf(53,plain, % 1.32/1.39 (~P3(f4(f4(f4(f4(f4(a3))))),f2(f1(x531)))+P2(f2(x531),f4(f4(f4(f4(f4(a3))))))), % 1.32/1.39 inference(scs_inference,[],[20,29,32])). % 1.32/1.39 cnf(58,plain, % 1.32/1.39 (~P3(f4(f4(f4(f4(f4(a3))))),f2(f1(x581)))+P2(f2(f1(x581)),f4(f4(f4(f4(a3)))))+P3(f4(f4(f4(f4(a3)))),f2(f1(x581)))), % 1.32/1.39 inference(scs_inference,[],[12,53,31])). % 1.32/1.39 cnf(59,plain, % 1.32/1.39 (P2(f2(f1(x591)),f4(f4(f4(f4(a3)))))+P3(f4(f4(f4(f4(a3)))),f2(f1(x591)))), % 1.32/1.39 inference(scs_inference,[],[58,51])). % 1.32/1.39 cnf(60,plain, % 1.32/1.39 (P3(f4(f4(f4(f4(a3)))),f2(f1(x601)))+~P3(f4(f4(f4(a3))),f2(f1(x601)))+P2(f2(f1(f1(x601))),f4(f4(f4(a3))))), % 1.32/1.39 inference(scs_inference,[],[59,38])). % 1.32/1.39 cnf(63,plain, % 1.32/1.39 (P2(f2(f1(x631)),f4(f4(f4(f4(a3)))))+~P3(f4(f4(f4(f4(a3)))),f2(x631))), % 1.32/1.39 inference(scs_inference,[],[20,59,30])). % 1.32/1.39 cnf(66,plain, % 1.32/1.39 (~P3(f4(f4(f4(f4(a3)))),f2(x661))+P3(f4(f4(f4(a3))),f2(f1(x661)))+P2(f2(f1(x661)),f4(f4(f4(a3))))), % 1.32/1.39 inference(scs_inference,[],[6,63,28])). % 1.32/1.39 cnf(67,plain, % 1.32/1.39 (P3(f4(f4(f4(a3))),f2(f1(f1(x671))))+~P3(f4(f4(f4(a3))),f2(f1(x671)))+P2(f2(f1(f1(x671))),f4(f4(f4(a3))))), % 1.32/1.39 inference(scs_inference,[],[66,60])). % 1.32/1.39 cnf(68,plain, % 1.32/1.39 (P2(f2(f1(f1(x681))),f4(f4(f4(a3))))+~P3(f4(f4(f4(a3))),f2(f1(x681)))), % 1.32/1.39 inference(scs_inference,[],[20,67,27])). % 1.32/1.39 cnf(76,plain, % 1.32/1.39 (~P3(f4(f4(f4(a3))),f2(f1(x761)))+P3(f4(f4(a3)),f2(f1(f1(x761))))+P2(f2(f1(f1(x761))),f4(f4(a3)))), % 1.32/1.39 inference(scs_inference,[],[6,68,26])). % 1.32/1.39 cnf(79,plain, % 1.32/1.39 (~P3(f4(f4(f4(a3))),f2(f1(x791)))+P3(f4(f4(a3)),f2(f1(f1(f1(x791)))))+P2(f2(f1(f1(f1(x791)))),f4(f4(a3)))), % 1.32/1.39 inference(scs_inference,[],[12,68,26])). % 1.32/1.39 cnf(81,plain, % 1.32/1.39 (P2(f2(f1(f1(x811))),f4(f4(f4(a3))))+P2(f2(f1(x811)),f4(f4(f4(a3))))+~P2(f2(x811),f4(f4(f4(f4(a3)))))), % 1.32/1.39 inference(scs_inference,[],[12,68,28])). % 1.32/1.39 cnf(84,plain, % 1.32/1.39 (P2(f2(f1(f1(x841))),f4(f4(f4(a3))))+P2(f2(f1(x841)),f4(f4(f4(a3))))+~P2(f2(f1(x841)),f4(f4(f4(f4(a3)))))), % 1.32/1.39 inference(scs_inference,[],[6,68,28])). % 1.32/1.39 cnf(86,plain, % 1.32/1.39 (P3(f4(f4(f4(f4(a3)))),f2(f1(x861)))+P2(f2(f1(f1(f1(x861)))),f4(f4(f4(a3))))+P2(f2(f1(f1(x861))),f4(f4(f4(a3))))), % 1.32/1.39 inference(scs_inference,[],[59,81])). % 1.32/1.39 cnf(87,plain, % 1.32/1.39 (P2(f2(f1(f1(x871))),f4(f4(f4(f4(a3)))))+P2(f2(f1(f1(f1(x871)))),f4(f4(f4(a3))))+P2(f2(f1(f1(x871))),f4(f4(f4(a3))))), % 1.32/1.39 inference(scs_inference,[],[86,63])). % 1.32/1.39 cnf(88,plain, % 1.32/1.39 (P2(f2(f1(f1(f1(x881)))),f4(f4(f4(a3))))+P2(f2(f1(f1(x881))),f4(f4(f4(a3))))), % 1.32/1.39 inference(scs_inference,[],[87,84])). % 1.32/1.39 cnf(90,plain, % 1.32/1.39 (P2(f2(f1(x901)),f4(f4(f4(f4(a3)))))+~P3(f4(f4(f4(f4(a3)))),f2(f1(f1(x901))))), % 1.32/1.39 inference(scs_inference,[],[20,59,30])). % 1.32/1.39 cnf(98,plain, % 1.32/1.39 (P3(f4(f4(f4(f4(a3)))),f2(f1(x981)))+P3(f4(f4(f4(a3))),f2(f1(x981)))+P2(f2(f1(x981)),f4(f4(f4(a3))))), % 1.32/1.39 inference(scs_inference,[],[6,59,28])). % 1.32/1.39 cnf(103,plain, % 1.32/1.39 (P2(f2(f1(f1(x1031))),f4(f4(f4(a3))))+P3(f4(f4(a3)),f2(f1(f1(f1(f1(x1031))))))+P2(f2(f1(f1(f1(f1(x1031))))),f4(f4(a3)))), % 1.32/1.39 inference(scs_inference,[],[12,88,26])). % 1.32/1.39 cnf(104,plain, % 1.32/1.39 (P2(f2(f1(f1(f1(x1041)))),f4(f4(f4(a3))))+P3(f4(f4(a3)),f2(f1(f1(f1(x1041)))))+P2(f2(f1(f1(f1(x1041)))),f4(f4(a3)))), % 1.32/1.39 inference(scs_inference,[],[12,88,26])). % 1.32/1.39 cnf(105,plain, % 1.32/1.39 (P2(f2(f1(f1(x1051))),f4(f4(f4(a3))))+P3(f4(f4(a3)),f2(f1(f1(f1(x1051)))))+P2(f2(f1(f1(f1(x1051)))),f4(f4(a3)))), % 1.32/1.39 inference(scs_inference,[],[6,88,26])). % 1.32/1.39 cnf(106,plain, % 1.32/1.39 (~P3(f4(f4(a3)),f2(f1(f1(x1061))))+P3(f4(f4(a3)),f2(f1(f1(f1(x1061)))))+P2(f2(f1(f1(f1(x1061)))),f4(f4(a3)))), % 1.32/1.39 inference(scs_inference,[],[105,37])). % 1.32/1.39 cnf(107,plain, % 1.32/1.39 (P2(f2(f1(f1(f1(x1071)))),f4(f4(a3)))+~P3(f4(f4(a3)),f2(f1(f1(x1071))))), % 1.32/1.39 inference(scs_inference,[],[20,106,25])). % 1.32/1.39 cnf(118,plain, % 1.32/1.39 (~P3(f4(f4(a3)),f2(f1(f1(x1181))))+P2(f2(f1(f1(f1(x1181)))),f4(a3))+P3(f4(a3),f2(f1(f1(f1(x1181)))))), % 1.32/1.39 inference(scs_inference,[],[6,107,23])). % 1.32/1.39 cnf(119,plain, % 1.32/1.39 (P2(f2(f1(f1(f1(x1191)))),f4(f4(a3)))+P2(f2(f1(f1(x1191))),f4(f4(a3)))+~P2(f2(f1(f1(x1191))),f4(f4(f4(a3))))), % 1.32/1.39 inference(scs_inference,[],[6,107,26])). % 1.32/1.39 cnf(120,plain, % 1.32/1.39 (P2(f2(f1(f1(f1(f1(x1201))))),f4(f4(a3)))+P3(f4(f4(a3)),f2(f1(f1(f1(x1201)))))+P2(f2(f1(f1(f1(x1201)))),f4(f4(a3)))), % 1.32/1.39 inference(scs_inference,[],[119,104])). % 1.32/1.39 cnf(121,plain, % 1.32/1.39 (P2(f2(f1(f1(f1(x1211)))),f4(f4(a3)))+P2(f2(f1(f1(f1(f1(x1211))))),f4(f4(a3)))), % 1.32/1.39 inference(scs_inference,[],[120,107])). % 1.32/1.39 cnf(123,plain, % 1.32/1.39 (~P3(f4(f4(a3)),f2(f1(f1(x1231))))+P2(f2(f1(f1(f1(f1(x1231))))),f4(a3))+P3(f4(a3),f2(f1(f1(f1(f1(x1231))))))), % 1.32/1.39 inference(scs_inference,[],[12,107,23])). % 1.32/1.39 cnf(126,plain, % 1.32/1.39 (P2(f2(f1(f1(f1(x1261)))),f4(f4(f4(a3))))+P3(f4(f4(a3)),f2(f1(f1(x1261))))+P2(f2(f1(f1(x1261))),f4(f4(a3)))), % 1.32/1.39 inference(scs_inference,[],[6,88,26])). % 1.32/1.39 cnf(127,plain, % 1.32/1.39 (~P3(f4(f4(f4(f4(a3)))),f2(f1(f1(x1271))))+P3(f4(f4(f4(a3))),f2(f1(f1(x1271))))+P2(f2(f1(f1(x1271))),f4(f4(f4(a3))))), % 1.32/1.39 inference(scs_inference,[],[12,90,28])). % 1.32/1.39 cnf(128,plain, % 1.32/1.39 (P3(f4(f4(f4(a3))),f2(f1(f1(x1281))))+P2(f2(f1(f1(x1281))),f4(f4(f4(a3))))), % 1.32/1.39 inference(scs_inference,[],[127,98])). % 1.32/1.39 cnf(136,plain, % 1.32/1.39 (P3(f4(f4(f4(a3))),f2(f1(f1(x1361))))+P3(f4(f4(a3)),f2(f1(f1(x1361))))+P2(f2(f1(f1(x1361))),f4(f4(a3)))), % 1.32/1.39 inference(scs_inference,[],[6,128,26])). % 1.32/1.39 cnf(143,plain, % 1.32/1.39 (P2(f2(f1(f1(f1(x1431)))),f4(f4(a3)))+P3(f4(a3),f2(f1(f1(f1(f1(x1431))))))+~P2(f2(f1(f1(f1(x1431)))),f4(a3))), % 1.32/1.39 inference(scs_inference,[],[121,46])). % 1.32/1.39 cnf(144,plain, % 1.32/1.39 (P3(f4(a3),f2(f1(f1(f1(f1(x1441))))))+~P2(f2(f1(f1(f1(x1441)))),f4(a3))), % 1.32/1.39 inference(scs_inference,[],[143,48])). % 1.32/1.39 cnf(145,plain, % 1.32/1.39 (~P2(f2(f1(f1(f1(x1451)))),f4(a3))+~P3(f4(a3),f2(f1(f1(f1(f1(f1(x1451)))))))), % 1.32/1.39 inference(scs_inference,[],[20,144,24])). % 1.32/1.39 cnf(164,plain, % 1.32/1.39 (~P2(f2(f1(f1(f1(x1641)))),f4(a3))+P2(f2(f1(f1(f1(f1(f1(x1641)))))),f4(a3))+~P2(f2(f1(f1(f1(f1(x1641))))),f4(f4(a3)))), % 1.32/1.39 inference(scs_inference,[],[12,145,23])). % 1.32/1.39 cnf(176,plain, % 1.32/1.39 (~P2(f2(f1(f1(f1(x1761)))),f4(a3))+P2(f2(f1(f1(f1(f1(f1(x1761)))))),f4(a3))+~P2(f2(f1(f1(f1(f1(f1(x1761)))))),f4(f4(a3)))), % 1.32/1.39 inference(scs_inference,[],[6,145,23])). % 1.32/1.39 cnf(183,plain, % 1.32/1.39 (P2(f2(f1(f1(f1(f1(f1(x1831)))))),f4(f4(a3)))+~P2(f2(f1(f1(f1(x1831)))),f4(a3))+P2(f2(f1(f1(f1(f1(f1(x1831)))))),f4(a3))), % 1.32/1.39 inference(scs_inference,[],[121,164])). % 1.32/1.39 cnf(184,plain, % 1.32/1.39 (~P2(f2(f1(f1(f1(x1841)))),f4(a3))+P2(f2(f1(f1(f1(f1(f1(x1841)))))),f4(a3))), % 1.32/1.39 inference(scs_inference,[],[183,176])). % 1.32/1.39 cnf(186,plain, % 1.32/1.39 (~P2(f2(f1(f1(f1(x1861)))),f4(a3))+P3(a3,f2(f1(f1(f1(f1(f1(f1(x1861))))))))), % 1.32/1.39 inference(scs_inference,[],[13,12,184,21])). % 1.32/1.39 cnf(189,plain, % 1.32/1.39 (~P2(f2(f1(f1(f1(x1891)))),f4(a3))+P3(a3,f2(f1(f1(f1(f1(f1(x1891)))))))), % 1.32/1.39 inference(scs_inference,[],[13,6,184,21])). % 1.32/1.39 cnf(191,plain, % 1.32/1.39 (~P2(f2(f1(f1(f1(x1911)))),f4(a3))+~P3(a3,f2(f1(f1(f1(f1(f1(f1(x1911))))))))), % 1.32/1.39 inference(scs_inference,[],[20,189,22])). % 1.32/1.39 cnf(205,plain, % 1.32/1.39 (P2(f2(f1(f1(f1(f1(f1(x2051)))))),f4(a3))+P3(f4(a3),f2(f1(f1(f1(x2051)))))+~P2(f2(f1(f1(x2051))),f4(f4(a3)))), % 1.32/1.39 inference(scs_inference,[],[12,184,23])). % 1.32/1.39 cnf(216,plain, % 1.32/1.39 (~P2(f2(f1(f1(f1(x2161)))),f4(a3))), % 1.32/1.39 inference(scs_inference,[],[186,191])). % 1.32/1.39 cnf(217,plain, % 1.32/1.39 (~P3(f4(f4(a3)),f2(f1(f1(x2171))))+P3(f4(a3),f2(f1(f1(f1(x2171)))))), % 1.32/1.39 inference(scs_inference,[],[216,118])). % 1.32/1.39 cnf(219,plain, % 1.32/1.39 (~P3(f4(f4(a3)),f2(f1(f1(x2191))))+~P3(f4(a3),f2(f1(f1(x2191))))), % 1.32/1.39 inference(scs_inference,[],[20,216,118,24])). % 1.32/1.39 cnf(227,plain, % 1.32/1.39 (~P3(f4(f4(f4(a3))),f2(f1(x2271)))+P2(f2(f1(f1(x2271))),f4(f4(a3)))+~P3(f4(a3),f2(f1(f1(x2271))))), % 1.32/1.39 inference(scs_inference,[],[219,76])). % 1.32/1.39 cnf(228,plain, % 1.32/1.39 (~P3(f4(f4(a3)),f2(f1(f1(x2281))))+P3(f4(a3),f2(f1(f1(f1(f1(x2281))))))), % 1.32/1.39 inference(scs_inference,[],[216,123])). % 1.32/1.39 cnf(232,plain, % 1.32/1.39 (~P3(f4(f4(a3)),f2(f1(f1(x2321))))+~P3(f4(a3),f2(f1(f1(f1(x2321)))))), % 1.32/1.39 inference(scs_inference,[],[20,216,123,219,76,79,103,104,105,126,136,227,24])). % 1.32/1.39 cnf(239,plain, % 1.32/1.39 (~P2(f2(f1(f1(x2391))),f4(f4(a3)))+P3(f4(a3),f2(f1(f1(f1(x2391)))))), % 1.32/1.39 inference(scs_inference,[],[216,205])). % 1.32/1.39 cnf(250,plain, % 1.32/1.39 (P2(f2(f1(f1(f1(f1(x2501))))),f4(f4(a3)))+P3(f4(a3),f2(f1(f1(f1(f1(x2501))))))), % 1.32/1.39 inference(scs_inference,[],[239,121])). % 1.32/1.39 cnf(285,plain, % 1.32/1.39 (~P3(f4(f4(f4(a3))),f2(f1(x2851)))+P2(f2(f1(f1(f1(x2851)))),f4(f4(a3)))+~P3(f4(a3),f2(f1(f1(f1(x2851)))))), % 1.32/1.39 inference(scs_inference,[],[219,79])). % 1.32/1.39 cnf(286,plain, % 1.32/1.39 (P2(f2(f1(f1(x2861))),f4(f4(f4(a3))))+P2(f2(f1(f1(f1(f1(x2861))))),f4(f4(a3)))+~P3(f4(a3),f2(f1(f1(f1(f1(x2861))))))), % 1.32/1.39 inference(scs_inference,[],[285,128])). % 1.32/1.39 cnf(287,plain, % 1.32/1.39 (P2(f2(f1(f1(x2871))),f4(f4(f4(a3))))+P2(f2(f1(f1(f1(f1(x2871))))),f4(f4(a3)))), % 1.32/1.39 inference(scs_inference,[],[286,250])). % 1.32/1.39 cnf(304,plain, % 1.32/1.39 (P2(f2(f1(f1(f1(x3041)))),f4(f4(f4(a3))))+P2(f2(f1(f1(f1(x3041)))),f4(f4(a3)))+~P3(f4(a3),f2(f1(f1(f1(x3041)))))), % 1.32/1.39 inference(scs_inference,[],[219,104])). % 1.32/1.39 cnf(305,plain, % 1.32/1.39 (P2(f2(f1(f1(f1(f1(x3051))))),f4(f4(f4(a3))))+P2(f2(f1(f1(f1(f1(x3051))))),f4(f4(a3)))), % 1.32/1.39 inference(scs_inference,[],[304,250])). % 1.32/1.39 cnf(306,plain, % 1.32/1.39 (P2(f2(f1(f1(f1(f1(x3061))))),f4(f4(a3)))+P3(f4(f4(a3)),f2(f1(f1(f1(f1(x3061))))))), % 1.32/1.39 inference(scs_inference,[],[6,305,26])). % 1.32/1.39 cnf(307,plain, % 1.32/1.39 (P3(f4(f4(a3)),f2(f1(f1(f1(f1(x3071))))))+P3(f4(a3),f2(f1(f1(f1(f1(f1(x3071)))))))), % 1.32/1.39 inference(scs_inference,[],[306,239])). % 1.32/1.39 cnf(308,plain, % 1.32/1.39 (P3(f4(a3),f2(f1(f1(f1(f1(f1(x3081)))))))), % 1.32/1.39 inference(scs_inference,[],[307,217])). % 1.32/1.39 cnf(323,plain, % 1.32/1.39 ($false), % 1.32/1.39 inference(scs_inference,[],[308,20,232,24,217,228,239,250,287,306]), % 1.32/1.39 ['proof']). % 1.32/1.39 % SZS output end Proof % 1.32/1.39 % Total time : 0.700000 s %------------------------------------------------------------------------------