%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : CSR113+18 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % Computer : n024.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 : Fri Jul 15 23:30:20 EDT 2022 % Result : Theorem 6.74s 6.96s % Output : Proof 6.74s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : CSR113+18 : TPTP v8.1.0. Released v4.0.0. % 0.11/0.13 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.13/0.34 % Computer : n024.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 600 % 0.13/0.34 % DateTime : Fri Jun 10 15:04:34 EDT 2022 % 0.13/0.34 % CPUTime : % 6.74/6.96 % SZS status Theorem % 6.74/6.96 (* PROOF-FOUND *) % 6.74/6.96 (* BEGIN-PROOF *) % 6.74/6.96 % SZS output start Proof % 6.74/6.96 1. (attr (c41) (c42)) (-. (attr (c41) (c42))) ### Axiom % 6.74/6.96 2. (loc (c8) (c53)) (-. (loc (c8) (c53))) ### Axiom % 6.74/6.96 3. (scar (c8) (c4)) (-. (scar (c8) (c4))) ### Axiom % 6.74/6.96 4. (sub (c42) (name_1_1)) (-. (sub (c42) (name_1_1))) ### Axiom % 6.74/6.96 5. (sub (c4) (freiheitsstatue_1_1)) (-. (sub (c4) (freiheitsstatue_1_1))) ### Axiom % 6.74/6.96 6. (subs (c8) (stehen_1_1)) (-. (subs (c8) (stehen_1_1))) ### Axiom % 6.74/6.96 7. (val (c42) (new_york_0)) (-. (val (c42) (new_york_0))) ### Axiom % 6.74/6.96 8. (-. ((attr (c41) (c42)) /\ ((loc (c8) (c53)) /\ ((scar (c8) (c4)) /\ ((sub (c42) (name_1_1)) /\ ((sub (c4) (freiheitsstatue_1_1)) /\ ((subs (c8) (stehen_1_1)) /\ (val (c42) (new_york_0))))))))) (val (c42) (new_york_0)) (subs (c8) (stehen_1_1)) (sub (c4) (freiheitsstatue_1_1)) (sub (c42) (name_1_1)) (scar (c8) (c4)) (loc (c8) (c53)) (attr (c41) (c42)) ### DisjTree 1 2 3 4 5 6 7 % 6.74/6.96 9. (-. (Ex X4, ((attr (c41) (c42)) /\ ((loc (c8) (c53)) /\ ((scar (c8) X4) /\ ((sub (c42) (name_1_1)) /\ ((sub X4 (freiheitsstatue_1_1)) /\ ((subs (c8) (stehen_1_1)) /\ (val (c42) (new_york_0)))))))))) (attr (c41) (c42)) (loc (c8) (c53)) (scar (c8) (c4)) (sub (c42) (name_1_1)) (sub (c4) (freiheitsstatue_1_1)) (subs (c8) (stehen_1_1)) (val (c42) (new_york_0)) ### NotExists 8 % 6.74/6.96 10. (-. (Ex X3, (Ex X4, ((attr (c41) (c42)) /\ ((loc X3 (c53)) /\ ((scar X3 X4) /\ ((sub (c42) (name_1_1)) /\ ((sub X4 (freiheitsstatue_1_1)) /\ ((subs X3 (stehen_1_1)) /\ (val (c42) (new_york_0))))))))))) (val (c42) (new_york_0)) (subs (c8) (stehen_1_1)) (sub (c4) (freiheitsstatue_1_1)) (sub (c42) (name_1_1)) (scar (c8) (c4)) (loc (c8) (c53)) (attr (c41) (c42)) ### NotExists 9 % 6.74/6.96 11. (-. (Ex X2, (Ex X3, (Ex X4, ((attr X2 (c42)) /\ ((loc X3 (c53)) /\ ((scar X3 X4) /\ ((sub (c42) (name_1_1)) /\ ((sub X4 (freiheitsstatue_1_1)) /\ ((subs X3 (stehen_1_1)) /\ (val (c42) (new_york_0)))))))))))) (attr (c41) (c42)) (loc (c8) (c53)) (scar (c8) (c4)) (sub (c42) (name_1_1)) (sub (c4) (freiheitsstatue_1_1)) (subs (c8) (stehen_1_1)) (val (c42) (new_york_0)) ### NotExists 10 % 6.74/6.96 12. (-. (Ex X1, (Ex X2, (Ex X3, (Ex X4, ((attr X2 X1) /\ ((loc X3 (c53)) /\ ((scar X3 X4) /\ ((sub X1 (name_1_1)) /\ ((sub X4 (freiheitsstatue_1_1)) /\ ((subs X3 (stehen_1_1)) /\ (val X1 (new_york_0))))))))))))) (val (c42) (new_york_0)) (subs (c8) (stehen_1_1)) (sub (c4) (freiheitsstatue_1_1)) (sub (c42) (name_1_1)) (scar (c8) (c4)) (loc (c8) (c53)) (attr (c41) (c42)) ### NotExists 11 % 6.74/6.96 13. (-. (Ex X0, (Ex X1, (Ex X2, (Ex X3, (Ex X4, ((attr X2 X1) /\ ((loc X3 X0) /\ ((scar X3 X4) /\ ((sub X1 (name_1_1)) /\ ((sub X4 (freiheitsstatue_1_1)) /\ ((subs X3 (stehen_1_1)) /\ (val X1 (new_york_0)))))))))))))) (attr (c41) (c42)) (loc (c8) (c53)) (scar (c8) (c4)) (sub (c42) (name_1_1)) (sub (c4) (freiheitsstatue_1_1)) (subs (c8) (stehen_1_1)) (val (c42) (new_york_0)) ### NotExists 12 % 6.74/6.96 14. ((supl (c34) (bekannt_1_1) (c35)) /\ ((prop (c4) (c34)) /\ ((sub (c4) (freiheitsstatue_1_1)) /\ ((attr (c41) (c42)) /\ ((sub (c41) (stadt__1_1)) /\ ((sub (c42) (name_1_1)) /\ ((val (c42) (new_york_0)) /\ ((mexp (c44) (c50)) /\ ((semrel (c44) (c8)) /\ ((subs (c44) (sehen_1_1)) /\ ((vor (c53) (c41)) /\ ((loc (c8) (c53)) /\ ((scar (c8) (c4)) /\ ((subs (c8) (stehen_1_1)) /\ ((assoc (freiheitsstatue_1_1) (freiheit_1_1)) /\ ((sub (freiheitsstatue_1_1) (statue_1_1)) /\ ((sort (c34) (tq)) /\ ((sort (bekannt_1_1) (nq)) /\ ((sort (c35) (o)) /\ ((card (c35) (card_c)) /\ ((etype (c35) (int1)) /\ ((etype (c35) (int2)) /\ ((fact (c35) (real)) /\ ((gener (c35) (gener_c)) /\ ((quant (c35) (quant_c)) /\ ((refer (c35) (refer_c)) /\ ((varia (c35) (varia_c)) /\ ((sort (c4) (d)) /\ ((card (c4) (int1)) /\ ((etype (c4) (int0)) /\ ((fact (c4) (real)) /\ ((gener (c4) (sp)) /\ ((quant (c4) (one)) /\ ((refer (c4) (det)) /\ ((varia (c4) (con)) /\ ((sort (freiheitsstatue_1_1) (d)) /\ ((card (freiheitsstatue_1_1) (int1)) /\ ((etype (freiheitsstatue_1_1) (int0)) /\ ((fact (freiheitsstatue_1_1) (real)) /\ ((gener (freiheitsstatue_1_1) (ge)) /\ ((quant (freiheitsstatue_1_1) (one)) /\ ((refer (freiheitsstatue_1_1) (refer_c)) /\ ((varia (freiheitsstatue_1_1) (varia_c)) /\ ((sort (c41) (d)) /\ ((sort (c41) (io)) /\ ((card (c41) (int1)) /\ ((etype (c41) (int0)) /\ ((fact (c41) (real)) /\ ((gener (c41) (sp)) /\ ((quant (c41) (one)) /\ ((refer (c41) (det)) /\ ((varia (c41) (con)) /\ ((sort (c42) (na)) /\ ((card (c42) (int1)) /\ ((etype (c42) (int0)) /\ ((fact (c42) (real)) /\ ((gener (c42) (sp)) /\ ((quant (c42) (one)) /\ ((refer (c42) (indet)) /\ ((varia (c42) (varia_c)) /\ ((sort (stadt__1_1) (d)) /\ ((sort (stadt__1_1) (io)) /\ ((card (stadt__1_1) (int1)) /\ ((etype (stadt__1_1) (int0)) /\ ((fact (stadt__1_1) (real)) /\ ((gener (stadt__1_1) (ge)) /\ ((quant (stadt__1_1) (one)) /\ ((refer (stadt__1_1) (refer_c)) /\ ((varia (stadt__1_1) (varia_c)) /\ ((sort (name_1_1) (na)) /\ ((card (name_1_1) (int1)) /\ ((etype (name_1_1) (int0)) /\ ((fact (name_1_1) (real)) /\ ((gener (name_1_1) (ge)) /\ ((quant (name_1_1) (one)) /\ ((refer (name_1_1) (refer_c)) /\ ((varia (name_1_1) (varia_c)) /\ ((sort (new_york_0) (fe)) /\ ((sort (c44) (dn)) /\ ((fact (c44) (real)) /\ ((gener (c44) (sp)) /\ ((sort (c50) (d)) /\ ((card (c50) (int1)) /\ ((etype (c50) (int0)) /\ ((fact (c50) (real)) /\ ((gener (c50) (sp)) /\ ((quant (c50) (one)) /\ ((refer (c50) (det)) /\ ((varia (c50) (varia_c)) /\ ((sort (c8) (st)) /\ ((fact (c8) (real)) /\ ((gener (c8) (sp)) /\ ((sort (sehen_1_1) (dn)) /\ ((fact (sehen_1_1) (real)) /\ ((gener (sehen_1_1) (ge)) /\ ((sort (c53) (l)) /\ ((card (c53) (int1)) /\ ((etype (c53) (int0)) /\ ((fact (c53) (real)) /\ ((gener (c53) (sp)) /\ ((quant (c53) (one)) /\ ((refer (c53) (det)) /\ ((varia (c53) (con)) /\ ((sort (stehen_1_1) (st)) /\ ((fact (stehen_1_1) (real)) /\ ((gener (stehen_1_1) (ge)) /\ ((sort (freiheit_1_1) (as)) /\ ((sort (freiheit_1_1) (io)) /\ ((card (freiheit_1_1) (int1)) /\ ((etype (freiheit_1_1) (int0)) /\ ((fact (freiheit_1_1) (real)) /\ ((gener (freiheit_1_1) (ge)) /\ ((quant (freiheit_1_1) (one)) /\ ((refer (freiheit_1_1) (refer_c)) /\ ((varia (freiheit_1_1) (varia_c)) /\ ((sort (statue_1_1) (d)) /\ ((card (statue_1_1) (int1)) /\ ((etype (statue_1_1) (int0)) /\ ((fact (statue_1_1) (real)) /\ ((gener (statue_1_1) (ge)) /\ ((quant (statue_1_1) (one)) /\ ((refer (statue_1_1) (refer_c)) /\ (varia (statue_1_1) (varia_c)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (-. (Ex X0, (Ex X1, (Ex X2, (Ex X3, (Ex X4, ((attr X2 X1) /\ ((loc X3 X0) /\ ((scar X3 X4) /\ ((sub X1 (name_1_1)) /\ ((sub X4 (freiheitsstatue_1_1)) /\ ((subs X3 (stehen_1_1)) /\ (val X1 (new_york_0)))))))))))))) ### ConjTree 13 % 6.74/6.96 % SZS output end Proof % 6.74/6.96 (* END-PROOF *) %------------------------------------------------------------------------------