%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : CSR114+6 : 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 : n023.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:26 EDT 2022 % Result : Theorem 6.65s 6.86s % Output : Proof 6.65s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.13 % Problem : CSR114+6 : TPTP v8.1.0. Released v4.0.0. % 0.08/0.13 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.13/0.35 % Computer : n023.cluster.edu % 0.13/0.35 % Model : x86_64 x86_64 % 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.35 % Memory : 8042.1875MB % 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.35 % CPULimit : 300 % 0.13/0.35 % WCLimit : 600 % 0.13/0.35 % DateTime : Sat Jun 11 12:46:22 EDT 2022 % 0.13/0.35 % CPUTime : % 6.65/6.86 % SZS status Theorem % 6.65/6.86 (* PROOF-FOUND *) % 6.65/6.86 (* BEGIN-PROOF *) % 6.65/6.86 % SZS output start Proof % 6.65/6.86 1. (attr (c5) (c7)) (-. (attr (c5) (c7))) ### Axiom % 6.65/6.86 2. (-. (Ex X1, (attr (c5) X1))) (attr (c5) (c7)) ### NotExists 1 % 6.65/6.86 3. (-. (Ex X0, (Ex X1, (attr X0 X1)))) (attr (c5) (c7)) ### NotExists 2 % 6.65/6.86 4. ((attr (c5) (c6)) /\ ((attr (c5) (c7)) /\ ((sub (c6) (tag_1_1)) /\ ((val (c6) (c3)) /\ ((sub (c7) (monat_1_1)) /\ ((val (c7) (c4)) /\ ((sort (c5) (t)) /\ ((card (c5) (int1)) /\ ((etype (c5) (int0)) /\ ((fact (c5) (real)) /\ ((gener (c5) (sp)) /\ ((quant (c5) (one)) /\ ((refer (c5) (det)) /\ ((varia (c5) (con)) /\ ((sort (c6) (me)) /\ ((sort (c6) (oa)) /\ ((sort (c6) (ta)) /\ ((card (c6) (card_c)) /\ ((etype (c6) (etype_c)) /\ ((fact (c6) (real)) /\ ((gener (c6) (sp)) /\ ((quant (c6) (quant_c)) /\ ((refer (c6) (refer_c)) /\ ((varia (c6) (varia_c)) /\ ((sort (c7) (me)) /\ ((sort (c7) (oa)) /\ ((sort (c7) (ta)) /\ ((card (c7) (card_c)) /\ ((etype (c7) (etype_c)) /\ ((fact (c7) (real)) /\ ((gener (c7) (sp)) /\ ((quant (c7) (quant_c)) /\ ((refer (c7) (refer_c)) /\ ((varia (c7) (varia_c)) /\ ((sort (tag_1_1) (me)) /\ ((sort (tag_1_1) (oa)) /\ ((sort (tag_1_1) (ta)) /\ ((card (tag_1_1) (card_c)) /\ ((etype (tag_1_1) (etype_c)) /\ ((fact (tag_1_1) (real)) /\ ((gener (tag_1_1) (ge)) /\ ((quant (tag_1_1) (quant_c)) /\ ((refer (tag_1_1) (refer_c)) /\ ((varia (tag_1_1) (varia_c)) /\ ((sort (c3) (nu)) /\ ((card (c3) (int9)) /\ ((sort (monat_1_1) (me)) /\ ((sort (monat_1_1) (oa)) /\ ((sort (monat_1_1) (ta)) /\ ((card (monat_1_1) (card_c)) /\ ((etype (monat_1_1) (etype_c)) /\ ((fact (monat_1_1) (real)) /\ ((gener (monat_1_1) (ge)) /\ ((quant (monat_1_1) (quant_c)) /\ ((refer (monat_1_1) (refer_c)) /\ ((varia (monat_1_1) (varia_c)) /\ ((sort (c4) (nu)) /\ (card (c4) (int11))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (-. (Ex X0, (Ex X1, (attr X0 X1)))) ### ConjTree 3 % 6.65/6.86 % SZS output end Proof % 6.65/6.86 (* END-PROOF *) %------------------------------------------------------------------------------