%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : CSR115+51 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % 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 : Sat Jul 16 00:03:18 EDT 2022 % Result : Theorem 3.02s 3.22s % Output : Proof 3.02s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : CSR115+51 : TPTP v8.1.0. Released v4.0.0. % 0.07/0.13 % Command : run_zenon %s %d % 0.13/0.34 % Computer : n011.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 : Sat Jun 11 08:08:31 EDT 2022 % 0.13/0.34 % CPUTime : % 3.02/3.22 (* PROOF-FOUND *) % 3.02/3.22 % SZS status Theorem % 3.02/3.22 (* BEGIN-PROOF *) % 3.02/3.22 % SZS output start Proof % 3.02/3.22 Theorem synth_qa07_007_mira_news_1302_a19984 : (exists X0 : zenon_U, (exists X1 : zenon_U, (exists X2 : zenon_U, (exists X3 : zenon_U, (exists X4 : zenon_U, (exists X5 : zenon_U, ((agt X3 X2)/\((attr X2 X1)/\((attr X4 X5)/\((obj X3 X0)/\((prop X0 (britisch__1_1))/\((sub X1 (name_1_1))/\((subs X3 (n374bernehmen_1_1))/\(val X1 (bmw_0))))))))))))))). % 3.02/3.22 Proof. % 3.02/3.22 apply NNPP. intro zenon_G. % 3.02/3.22 apply (zenon_and_s _ _ ave07_era5_synth_qa07_007_mira_news_1302_a19984). zenon_intro zenon_H27ce. zenon_intro zenon_H27cd. % 3.02/3.22 apply (zenon_and_s _ _ zenon_H27cd). zenon_intro zenon_H27d0. zenon_intro zenon_H27cf. % 3.02/3.22 apply (zenon_and_s _ _ zenon_H27cf). zenon_intro zenon_H27d2. zenon_intro zenon_H27d1. % 3.02/3.22 apply (zenon_and_s _ _ zenon_H27d1). zenon_intro zenon_H27d4. zenon_intro zenon_H27d3. % 3.02/3.22 apply (zenon_and_s _ _ zenon_H27d3). zenon_intro zenon_H27d6. zenon_intro zenon_H27d5. % 3.02/3.22 apply (zenon_and_s _ _ zenon_H27d5). zenon_intro zenon_H27d8. zenon_intro zenon_H27d7. % 3.02/3.22 apply (zenon_and_s _ _ zenon_H27d7). zenon_intro zenon_H27da. zenon_intro zenon_H27d9. % 3.02/3.22 apply (zenon_and_s _ _ zenon_H27d9). zenon_intro zenon_H27dc. zenon_intro zenon_H27db. % 3.02/3.22 apply (zenon_and_s _ _ zenon_H27db). zenon_intro zenon_H27de. zenon_intro zenon_H27dd. % 3.02/3.22 apply (zenon_and_s _ _ zenon_H27dd). zenon_intro zenon_H27e0. zenon_intro zenon_H27df. % 3.02/3.22 apply (zenon_and_s _ _ zenon_H27df). zenon_intro zenon_H27e2. zenon_intro zenon_H27e1. % 3.02/3.22 apply (zenon_and_s _ _ zenon_H27e1). zenon_intro zenon_H27e4. zenon_intro zenon_H27e3. % 3.02/3.22 apply (zenon_and_s _ _ zenon_H27e3). zenon_intro zenon_H27e6. zenon_intro zenon_H27e5. % 3.02/3.22 apply (zenon_and_s _ _ zenon_H27e5). zenon_intro zenon_H27e8. zenon_intro zenon_H27e7. % 3.02/3.22 apply (zenon_and_s _ _ zenon_H27e7). zenon_intro zenon_H27ea. zenon_intro zenon_H27e9. % 3.02/3.22 apply (zenon_and_s _ _ zenon_H27e9). zenon_intro zenon_H27ec. zenon_intro zenon_H27eb. % 3.02/3.22 apply (zenon_and_s _ _ zenon_H27eb). zenon_intro zenon_H27ee. zenon_intro zenon_H27ed. % 3.02/3.22 apply (zenon_and_s _ _ zenon_H27ed). zenon_intro zenon_H27f0. zenon_intro zenon_H27ef. % 3.02/3.22 apply (zenon_and_s _ _ zenon_H27ef). zenon_intro zenon_H27f2. zenon_intro zenon_H27f1. % 3.02/3.22 apply zenon_G. exists (c218). apply NNPP. zenon_intro zenon_H27f3. % 3.02/3.22 apply zenon_H27f3. exists (c166). apply NNPP. zenon_intro zenon_H27f4. % 3.02/3.22 apply zenon_H27f4. exists (c165). apply NNPP. zenon_intro zenon_H27f5. % 3.02/3.22 apply zenon_H27f5. exists (c163). apply NNPP. zenon_intro zenon_H27f6. % 3.02/3.22 apply zenon_H27f6. exists (c165). apply NNPP. zenon_intro zenon_H27f7. % 3.02/3.22 apply zenon_H27f7. exists (c166). apply NNPP. zenon_intro zenon_H27f8. % 3.02/3.22 apply (zenon_notand_s _ _ zenon_H27f8); [ zenon_intro zenon_H27fa | zenon_intro zenon_H27f9 ]. % 3.02/3.22 exact (zenon_H27fa zenon_H27de). % 3.02/3.22 apply (zenon_notand_s _ _ zenon_H27f9); [ zenon_intro zenon_H27fc | zenon_intro zenon_H27fb ]. % 3.02/3.22 exact (zenon_H27fc zenon_H27e4). % 3.02/3.22 apply (zenon_notand_s _ _ zenon_H27fb); [ zenon_intro zenon_H27fc | zenon_intro zenon_H27fd ]. % 3.02/3.22 exact (zenon_H27fc zenon_H27e4). % 3.02/3.22 apply (zenon_notand_s _ _ zenon_H27fd); [ zenon_intro zenon_H27ff | zenon_intro zenon_H27fe ]. % 3.02/3.22 exact (zenon_H27ff zenon_H27e0). % 3.02/3.22 apply (zenon_notand_s _ _ zenon_H27fe); [ zenon_intro zenon_H2801 | zenon_intro zenon_H2800 ]. % 3.02/3.22 exact (zenon_H2801 zenon_H27f2). % 3.02/3.22 apply (zenon_notand_s _ _ zenon_H2800); [ zenon_intro zenon_H2803 | zenon_intro zenon_H2802 ]. % 3.02/3.22 exact (zenon_H2803 zenon_H27ea). % 3.02/3.22 apply (zenon_notand_s _ _ zenon_H2802); [ zenon_intro zenon_H2805 | zenon_intro zenon_H2804 ]. % 3.02/3.22 exact (zenon_H2805 zenon_H27e2). % 3.02/3.22 exact (zenon_H2804 zenon_H27ec). % 3.02/3.22 Qed. % 3.02/3.22 % SZS output end Proof % 3.02/3.22 (* END-PROOF *) % 3.02/3.22 nodes searched: 73621 % 3.02/3.22 max branch formulas: 82000 % 3.02/3.22 proof nodes created: 35 % 3.02/3.22 formulas created: 999817 % 3.02/3.22 %------------------------------------------------------------------------------