%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : PUZ159_1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n015.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 : 300s % DateTime : Tue May 5 06:49:04 PM UTC 2026 % Result : Theorem 4.63s 4.83s % Output : Proof 4.73s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : PUZ159_1 : TPTP v9.3.0. Released v9.3.0. % 0.11/0.13 % Command : duper %s % 0.17/0.34 % Computer : n015.cluster.edu % 0.17/0.34 % Model : x86_64 x86_64 % 0.17/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.17/0.34 % Memory : 8042.1875MB % 0.17/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.17/0.34 % CPULimit : 300 % 0.17/0.34 % WCLimit : 300 % 0.17/0.35 % DateTime : Tue May 5 05:00:46 EDT 2026 % 0.17/0.35 % CPUTime : % 4.63/4.83 SZS status Theorem for theBenchmark.p % 4.63/4.83 SZS output start Proof for theBenchmark.p % 4.63/4.83 Clause #3 (by assumption #[]): Eq (∀ (E : event), armistice E → contentiousEvent E) True % 4.63/4.83 Clause #4 (by assumption #[]): Eq (∀ (E : event), armistice E → diplomaticEvent E) True % 4.63/4.83 Clause #5 (by assumption #[]): Eq (∀ (X Y Z : geographicalRegion), And (subRegions X Y) (subRegions Y Z) → subRegions X Z) True % 4.63/4.83 Clause #6 (by assumption #[]): Eq (∀ (X Y : geographicalRegion) (Z : event), And (eventOccursAt Z X) (subRegions Y X) → eventOccursAt Z Y) True % 4.63/4.83 Clause #7 (by assumption #[]): Eq (subRegions picardy rethondesCompiegne) True % 4.63/4.83 Clause #8 (by assumption #[]): Eq (subRegions hautsDeFrance picardy) True % 4.63/4.83 Clause #9 (by assumption #[]): Eq (subRegions france hautsDeFrance) True % 4.63/4.83 Clause #10 (by assumption #[]): Eq % 4.63/4.83 (∀ (CC : constrCont) (PR LT BW : govt), % 4.63/4.83 And (narrativeSuccessor CC PR BW) (narrativeSuccessor CC BW LT) → narrativeSuccessor CC PR LT) % 4.63/4.83 True % 4.63/4.83 Clause #13 (by assumption #[]): Eq (narrativeSuccessor germania thirdReich alliedOccupiedGermany) True % 4.63/4.83 Clause #14 (by assumption #[]): Eq (narrativeSuccessor germania alliedOccupiedGermany federalGermanRepublic) True % 4.63/4.83 Clause #32 (by assumption #[]): Eq (armistice armistice1940) True % 4.63/4.83 Clause #33 (by assumption #[]): Eq (eventOccursAt armistice1940 rethondesCompiegne) True % 4.63/4.83 Clause #35 (by assumption #[]): Eq (govtRepresentedBy armistice1940 thirdReich hitler) True % 4.63/4.83 Clause #37 (by assumption #[]): Eq (seatingEvent armistice1940GermanSeating) True % 4.63/4.83 Clause #38 (by assumption #[]): Eq (subEvents armistice1940 armistice1940GermanSeating) True % 4.63/4.83 Clause #39 (by assumption #[]): Eq (performedBy armistice1940GermanSeating hitler) True % 4.63/4.83 Clause #40 (by assumption #[]): Eq (seatedAtSide armistice1940GermanSeating cwlTableSideA) True % 4.63/4.83 Clause #47 (by assumption #[]): Eq (eventOccursAt compiegneVisit2018 rethondesCompiegne) True % 4.63/4.83 Clause #49 (by assumption #[]): Eq (friendlyEvent compiegneVisit2018) True % 4.63/4.83 Clause #50 (by assumption #[]): Eq (govtRepresentedBy compiegneVisit2018 federalGermanRepublic merkel) True % 4.63/4.83 Clause #52 (by assumption #[]): Eq (endsBeforeStartOf armistice1940 compiegneVisit2018) True % 4.63/4.83 Clause #53 (by assumption #[]): Eq % 4.63/4.83 (∀ (DE VE : event) (LOC : geographicalRegion), % 4.63/4.83 And (And (And (diplomaticEvent DE) (eventOccursAt DE LOC)) (eventOccursAt VE LOC)) (endsBeforeStartOf DE VE) → % 4.63/4.83 pastColocatedDiplomaticEvent VE DE) % 4.63/4.83 True % 4.63/4.83 Clause #54 (by assumption #[]): Eq % 4.63/4.83 (∀ (P RP : person) (PASTGOVT GOVT : govt) (CC : constrCont) (VE DE SE : event) (TS : table_side), % 4.63/4.83 And % 4.63/4.83 (And % 4.63/4.83 (And % 4.63/4.83 (And % 4.63/4.83 (And % 4.63/4.83 (And % 4.63/4.83 (And (And (And (pastColocatedDiplomaticEvent VE DE) (contentiousEvent DE)) (subEvents DE SE)) % 4.63/4.83 (seatingEvent SE)) % 4.63/4.83 (performedBy SE RP)) % 4.63/4.83 (seatedAtSide SE TS)) % 4.63/4.83 (govtRepresentedBy DE PASTGOVT RP)) % 4.63/4.83 (narrativeSuccessor CC PASTGOVT GOVT)) % 4.63/4.83 (friendlyEvent VE)) % 4.63/4.83 (govtRepresentedBy VE GOVT P) → % 4.63/4.83 avoidTableSide P VE TS) % 4.63/4.83 True % 4.63/4.83 Clause #55 (by assumption #[]): Eq (Not (avoidTableSide merkel compiegneVisit2018 cwlTableSideA)) True % 4.63/4.83 Clause #68 (by clausification #[3]): ∀ (a : event), Eq (armistice a → contentiousEvent a) True % 4.63/4.83 Clause #69 (by clausification #[68]): ∀ (a : event), Or (Eq (armistice a) False) (Eq (contentiousEvent a) True) % 4.63/4.83 Clause #70 (by superposition #[69, 32]): Or (Eq (contentiousEvent armistice1940) True) (Eq False True) % 4.63/4.83 Clause #72 (by clausification #[4]): ∀ (a : event), Eq (armistice a → diplomaticEvent a) True % 4.63/4.83 Clause #73 (by clausification #[72]): ∀ (a : event), Or (Eq (armistice a) False) (Eq (diplomaticEvent a) True) % 4.63/4.83 Clause #74 (by superposition #[73, 32]): Or (Eq (diplomaticEvent armistice1940) True) (Eq False True) % 4.63/4.83 Clause #77 (by clausification #[5]): ∀ (a : geographicalRegion), % 4.63/4.83 Eq (∀ (Y Z : geographicalRegion), And (subRegions a Y) (subRegions Y Z) → subRegions a Z) True % 4.63/4.83 Clause #78 (by clausification #[77]): ∀ (a a_1 : geographicalRegion), % 4.63/4.83 Eq (∀ (Z : geographicalRegion), And (subRegions a a_1) (subRegions a_1 Z) → subRegions a Z) True % 4.63/4.85 Clause #79 (by clausification #[78]): ∀ (a a_1 a_2 : geographicalRegion), Eq (And (subRegions a a_1) (subRegions a_1 a_2) → subRegions a a_2) True % 4.63/4.85 Clause #80 (by clausification #[79]): ∀ (a a_1 a_2 : geographicalRegion), % 4.63/4.85 Or (Eq (And (subRegions a a_1) (subRegions a_1 a_2)) False) (Eq (subRegions a a_2) True) % 4.63/4.85 Clause #81 (by clausification #[80]): ∀ (a a_1 a_2 : geographicalRegion), % 4.63/4.85 Or (Eq (subRegions a a_1) True) (Or (Eq (subRegions a a_2) False) (Eq (subRegions a_2 a_1) False)) % 4.63/4.85 Clause #82 (by superposition #[81, 9]): ∀ (a : geographicalRegion), % 4.63/4.85 Or (Eq (subRegions france a) True) (Or (Eq (subRegions hautsDeFrance a) False) (Eq False True)) % 4.63/4.85 Clause #83 (by superposition #[81, 8]): ∀ (a : geographicalRegion), % 4.63/4.85 Or (Eq (subRegions hautsDeFrance a) True) (Or (Eq (subRegions picardy a) False) (Eq False True)) % 4.63/4.85 Clause #86 (by clausification #[6]): ∀ (a : geographicalRegion), % 4.63/4.85 Eq (∀ (Y : geographicalRegion) (Z : event), And (eventOccursAt Z a) (subRegions Y a) → eventOccursAt Z Y) True % 4.63/4.85 Clause #87 (by clausification #[86]): ∀ (a a_1 : geographicalRegion), % 4.63/4.85 Eq (∀ (Z : event), And (eventOccursAt Z a) (subRegions a_1 a) → eventOccursAt Z a_1) True % 4.63/4.85 Clause #88 (by clausification #[87]): ∀ (a : event) (a_1 a_2 : geographicalRegion), % 4.63/4.85 Eq (And (eventOccursAt a a_1) (subRegions a_2 a_1) → eventOccursAt a a_2) True % 4.63/4.85 Clause #89 (by clausification #[88]): ∀ (a : event) (a_1 a_2 : geographicalRegion), % 4.63/4.85 Or (Eq (And (eventOccursAt a a_1) (subRegions a_2 a_1)) False) (Eq (eventOccursAt a a_2) True) % 4.63/4.85 Clause #90 (by clausification #[89]): ∀ (a : event) (a_1 a_2 : geographicalRegion), % 4.63/4.85 Or (Eq (eventOccursAt a a_1) True) (Or (Eq (eventOccursAt a a_2) False) (Eq (subRegions a_1 a_2) False)) % 4.63/4.85 Clause #91 (by superposition #[90, 33]): ∀ (a : geographicalRegion), % 4.63/4.85 Or (Eq (eventOccursAt armistice1940 a) True) (Or (Eq (subRegions a rethondesCompiegne) False) (Eq False True)) % 4.63/4.85 Clause #93 (by superposition #[90, 47]): ∀ (a : geographicalRegion), % 4.63/4.85 Or (Eq (eventOccursAt compiegneVisit2018 a) True) (Or (Eq (subRegions a rethondesCompiegne) False) (Eq False True)) % 4.63/4.85 Clause #94 (by clausification #[10]): ∀ (a : constrCont), % 4.63/4.85 Eq (∀ (PR LT BW : govt), And (narrativeSuccessor a PR BW) (narrativeSuccessor a BW LT) → narrativeSuccessor a PR LT) % 4.63/4.85 True % 4.63/4.85 Clause #95 (by clausification #[94]): ∀ (a : constrCont) (a_1 : govt), % 4.63/4.85 Eq (∀ (LT BW : govt), And (narrativeSuccessor a a_1 BW) (narrativeSuccessor a BW LT) → narrativeSuccessor a a_1 LT) % 4.63/4.85 True % 4.63/4.85 Clause #96 (by clausification #[95]): ∀ (a : constrCont) (a_1 a_2 : govt), % 4.63/4.85 Eq (∀ (BW : govt), And (narrativeSuccessor a a_1 BW) (narrativeSuccessor a BW a_2) → narrativeSuccessor a a_1 a_2) % 4.63/4.85 True % 4.63/4.85 Clause #97 (by clausification #[96]): ∀ (a : constrCont) (a_1 a_2 a_3 : govt), % 4.63/4.85 Eq (And (narrativeSuccessor a a_1 a_2) (narrativeSuccessor a a_2 a_3) → narrativeSuccessor a a_1 a_3) True % 4.63/4.85 Clause #98 (by clausification #[97]): ∀ (a : constrCont) (a_1 a_2 a_3 : govt), % 4.63/4.85 Or (Eq (And (narrativeSuccessor a a_1 a_2) (narrativeSuccessor a a_2 a_3)) False) % 4.63/4.85 (Eq (narrativeSuccessor a a_1 a_3) True) % 4.63/4.85 Clause #99 (by clausification #[98]): ∀ (a : constrCont) (a_1 a_2 a_3 : govt), % 4.63/4.85 Or (Eq (narrativeSuccessor a a_1 a_2) True) % 4.63/4.85 (Or (Eq (narrativeSuccessor a a_1 a_3) False) (Eq (narrativeSuccessor a a_3 a_2) False)) % 4.63/4.85 Clause #103 (by superposition #[99, 13]): ∀ (a : govt), % 4.63/4.85 Or (Eq (narrativeSuccessor germania thirdReich a) True) % 4.63/4.85 (Or (Eq (narrativeSuccessor germania alliedOccupiedGermany a) False) (Eq False True)) % 4.63/4.85 Clause #105 (by clausification #[74]): Eq (diplomaticEvent armistice1940) True % 4.63/4.85 Clause #108 (by clausification #[70]): Eq (contentiousEvent armistice1940) True % 4.63/4.85 Clause #112 (by clausification #[55]): Eq (avoidTableSide merkel compiegneVisit2018 cwlTableSideA) False % 4.63/4.85 Clause #113 (by clausification #[53]): ∀ (a : event), % 4.63/4.85 Eq % 4.63/4.85 (∀ (VE : event) (LOC : geographicalRegion), % 4.63/4.85 And (And (And (diplomaticEvent a) (eventOccursAt a LOC)) (eventOccursAt VE LOC)) (endsBeforeStartOf a VE) → % 4.63/4.85 pastColocatedDiplomaticEvent VE a) % 4.63/4.86 True % 4.63/4.86 Clause #114 (by clausification #[113]): ∀ (a a_1 : event), % 4.63/4.86 Eq % 4.63/4.86 (∀ (LOC : geographicalRegion), % 4.63/4.86 And (And (And (diplomaticEvent a) (eventOccursAt a LOC)) (eventOccursAt a_1 LOC)) (endsBeforeStartOf a a_1) → % 4.63/4.86 pastColocatedDiplomaticEvent a_1 a) % 4.63/4.86 True % 4.63/4.86 Clause #115 (by clausification #[114]): ∀ (a : event) (a_1 : geographicalRegion) (a_2 : event), % 4.63/4.86 Eq % 4.63/4.86 (And (And (And (diplomaticEvent a) (eventOccursAt a a_1)) (eventOccursAt a_2 a_1)) (endsBeforeStartOf a a_2) → % 4.63/4.86 pastColocatedDiplomaticEvent a_2 a) % 4.63/4.86 True % 4.63/4.86 Clause #116 (by clausification #[115]): ∀ (a : event) (a_1 : geographicalRegion) (a_2 : event), % 4.63/4.86 Or % 4.63/4.86 (Eq (And (And (And (diplomaticEvent a) (eventOccursAt a a_1)) (eventOccursAt a_2 a_1)) (endsBeforeStartOf a a_2)) % 4.63/4.86 False) % 4.63/4.86 (Eq (pastColocatedDiplomaticEvent a_2 a) True) % 4.63/4.86 Clause #117 (by clausification #[116]): ∀ (a a_1 : event) (a_2 : geographicalRegion), % 4.63/4.86 Or (Eq (pastColocatedDiplomaticEvent a a_1) True) % 4.63/4.86 (Or (Eq (And (And (diplomaticEvent a_1) (eventOccursAt a_1 a_2)) (eventOccursAt a a_2)) False) % 4.63/4.86 (Eq (endsBeforeStartOf a_1 a) False)) % 4.63/4.86 Clause #118 (by clausification #[117]): ∀ (a a_1 : event) (a_2 : geographicalRegion), % 4.63/4.86 Or (Eq (pastColocatedDiplomaticEvent a a_1) True) % 4.63/4.86 (Or (Eq (endsBeforeStartOf a_1 a) False) % 4.63/4.86 (Or (Eq (And (diplomaticEvent a_1) (eventOccursAt a_1 a_2)) False) (Eq (eventOccursAt a a_2) False))) % 4.63/4.86 Clause #119 (by clausification #[118]): ∀ (a a_1 : event) (a_2 : geographicalRegion), % 4.63/4.86 Or (Eq (pastColocatedDiplomaticEvent a a_1) True) % 4.63/4.86 (Or (Eq (endsBeforeStartOf a_1 a) False) % 4.63/4.86 (Or (Eq (eventOccursAt a a_2) False) (Or (Eq (diplomaticEvent a_1) False) (Eq (eventOccursAt a_1 a_2) False)))) % 4.63/4.86 Clause #120 (by superposition #[119, 52]): ∀ (a : geographicalRegion), % 4.63/4.86 Or (Eq (pastColocatedDiplomaticEvent compiegneVisit2018 armistice1940) True) % 4.63/4.86 (Or (Eq (eventOccursAt compiegneVisit2018 a) False) % 4.63/4.86 (Or (Eq (diplomaticEvent armistice1940) False) (Or (Eq (eventOccursAt armistice1940 a) False) (Eq False True)))) % 4.63/4.86 Clause #122 (by clausification #[93]): ∀ (a : geographicalRegion), % 4.63/4.86 Or (Eq (eventOccursAt compiegneVisit2018 a) True) (Eq (subRegions a rethondesCompiegne) False) % 4.63/4.86 Clause #123 (by superposition #[122, 7]): Or (Eq (eventOccursAt compiegneVisit2018 picardy) True) (Eq False True) % 4.63/4.86 Clause #124 (by clausification #[123]): Eq (eventOccursAt compiegneVisit2018 picardy) True % 4.63/4.86 Clause #125 (by superposition #[124, 90]): ∀ (a : geographicalRegion), % 4.63/4.86 Or (Eq (eventOccursAt compiegneVisit2018 a) True) (Or (Eq True False) (Eq (subRegions a picardy) False)) % 4.63/4.86 Clause #126 (by clausification #[125]): ∀ (a : geographicalRegion), Or (Eq (eventOccursAt compiegneVisit2018 a) True) (Eq (subRegions a picardy) False) % 4.63/4.86 Clause #127 (by superposition #[126, 8]): Or (Eq (eventOccursAt compiegneVisit2018 hautsDeFrance) True) (Eq False True) % 4.63/4.86 Clause #128 (by clausification #[127]): Eq (eventOccursAt compiegneVisit2018 hautsDeFrance) True % 4.63/4.86 Clause #129 (by superposition #[128, 90]): ∀ (a : geographicalRegion), % 4.63/4.86 Or (Eq (eventOccursAt compiegneVisit2018 a) True) (Or (Eq True False) (Eq (subRegions a hautsDeFrance) False)) % 4.63/4.86 Clause #130 (by clausification #[129]): ∀ (a : geographicalRegion), Or (Eq (eventOccursAt compiegneVisit2018 a) True) (Eq (subRegions a hautsDeFrance) False) % 4.63/4.86 Clause #131 (by superposition #[130, 9]): Or (Eq (eventOccursAt compiegneVisit2018 france) True) (Eq False True) % 4.63/4.86 Clause #132 (by clausification #[54]): ∀ (a : person), % 4.63/4.86 Eq % 4.63/4.86 (∀ (RP : person) (PASTGOVT GOVT : govt) (CC : constrCont) (VE DE SE : event) (TS : table_side), % 4.63/4.86 And % 4.63/4.86 (And % 4.63/4.86 (And % 4.63/4.86 (And % 4.63/4.86 (And % 4.63/4.86 (And % 4.63/4.86 (And (And (And (pastColocatedDiplomaticEvent VE DE) (contentiousEvent DE)) (subEvents DE SE)) % 4.63/4.86 (seatingEvent SE)) % 4.63/4.86 (performedBy SE RP)) % 4.63/4.86 (seatedAtSide SE TS)) % 4.63/4.86 (govtRepresentedBy DE PASTGOVT RP)) % 4.63/4.86 (narrativeSuccessor CC PASTGOVT GOVT)) % 4.63/4.86 (friendlyEvent VE)) % 4.63/4.86 (govtRepresentedBy VE GOVT a) → % 4.63/4.88 avoidTableSide a VE TS) % 4.63/4.88 True % 4.63/4.88 Clause #133 (by clausification #[132]): ∀ (a a_1 : person), % 4.63/4.88 Eq % 4.63/4.88 (∀ (PASTGOVT GOVT : govt) (CC : constrCont) (VE DE SE : event) (TS : table_side), % 4.63/4.88 And % 4.63/4.88 (And % 4.63/4.88 (And % 4.63/4.88 (And % 4.63/4.88 (And % 4.63/4.88 (And % 4.63/4.88 (And (And (And (pastColocatedDiplomaticEvent VE DE) (contentiousEvent DE)) (subEvents DE SE)) % 4.63/4.88 (seatingEvent SE)) % 4.63/4.88 (performedBy SE a)) % 4.63/4.88 (seatedAtSide SE TS)) % 4.63/4.88 (govtRepresentedBy DE PASTGOVT a)) % 4.63/4.88 (narrativeSuccessor CC PASTGOVT GOVT)) % 4.63/4.88 (friendlyEvent VE)) % 4.63/4.88 (govtRepresentedBy VE GOVT a_1) → % 4.63/4.88 avoidTableSide a_1 VE TS) % 4.63/4.88 True % 4.63/4.88 Clause #134 (by clausification #[133]): ∀ (a : person) (a_1 : govt) (a_2 : person), % 4.63/4.88 Eq % 4.63/4.88 (∀ (GOVT : govt) (CC : constrCont) (VE DE SE : event) (TS : table_side), % 4.63/4.88 And % 4.63/4.88 (And % 4.63/4.88 (And % 4.63/4.88 (And % 4.63/4.88 (And % 4.63/4.88 (And % 4.63/4.88 (And (And (And (pastColocatedDiplomaticEvent VE DE) (contentiousEvent DE)) (subEvents DE SE)) % 4.63/4.88 (seatingEvent SE)) % 4.63/4.88 (performedBy SE a)) % 4.63/4.88 (seatedAtSide SE TS)) % 4.63/4.88 (govtRepresentedBy DE a_1 a)) % 4.63/4.88 (narrativeSuccessor CC a_1 GOVT)) % 4.63/4.88 (friendlyEvent VE)) % 4.63/4.88 (govtRepresentedBy VE GOVT a_2) → % 4.63/4.88 avoidTableSide a_2 VE TS) % 4.63/4.88 True % 4.63/4.88 Clause #135 (by clausification #[134]): ∀ (a : person) (a_1 a_2 : govt) (a_3 : person), % 4.63/4.88 Eq % 4.63/4.88 (∀ (CC : constrCont) (VE DE SE : event) (TS : table_side), % 4.63/4.88 And % 4.63/4.88 (And % 4.63/4.88 (And % 4.63/4.88 (And % 4.63/4.88 (And % 4.63/4.88 (And % 4.63/4.88 (And (And (And (pastColocatedDiplomaticEvent VE DE) (contentiousEvent DE)) (subEvents DE SE)) % 4.63/4.88 (seatingEvent SE)) % 4.63/4.88 (performedBy SE a)) % 4.63/4.88 (seatedAtSide SE TS)) % 4.63/4.88 (govtRepresentedBy DE a_1 a)) % 4.63/4.88 (narrativeSuccessor CC a_1 a_2)) % 4.63/4.88 (friendlyEvent VE)) % 4.63/4.88 (govtRepresentedBy VE a_2 a_3) → % 4.63/4.88 avoidTableSide a_3 VE TS) % 4.63/4.88 True % 4.63/4.88 Clause #136 (by clausification #[135]): ∀ (a : person) (a_1 : govt) (a_2 : constrCont) (a_3 : govt) (a_4 : person), % 4.63/4.88 Eq % 4.63/4.88 (∀ (VE DE SE : event) (TS : table_side), % 4.63/4.88 And % 4.63/4.88 (And % 4.63/4.88 (And % 4.63/4.88 (And % 4.63/4.88 (And % 4.63/4.88 (And % 4.63/4.88 (And (And (And (pastColocatedDiplomaticEvent VE DE) (contentiousEvent DE)) (subEvents DE SE)) % 4.63/4.88 (seatingEvent SE)) % 4.63/4.88 (performedBy SE a)) % 4.63/4.88 (seatedAtSide SE TS)) % 4.63/4.88 (govtRepresentedBy DE a_1 a)) % 4.63/4.88 (narrativeSuccessor a_2 a_1 a_3)) % 4.63/4.88 (friendlyEvent VE)) % 4.63/4.88 (govtRepresentedBy VE a_3 a_4) → % 4.63/4.88 avoidTableSide a_4 VE TS) % 4.63/4.88 True % 4.63/4.88 Clause #137 (by clausification #[136]): ∀ (a : event) (a_1 : person) (a_2 : govt) (a_3 : constrCont) (a_4 : govt) (a_5 : person), % 4.63/4.88 Eq % 4.63/4.88 (∀ (DE SE : event) (TS : table_side), % 4.63/4.88 And % 4.63/4.88 (And % 4.63/4.88 (And % 4.63/4.88 (And % 4.63/4.88 (And % 4.63/4.88 (And % 4.63/4.88 (And (And (And (pastColocatedDiplomaticEvent a DE) (contentiousEvent DE)) (subEvents DE SE)) % 4.63/4.88 (seatingEvent SE)) % 4.63/4.88 (performedBy SE a_1)) % 4.63/4.88 (seatedAtSide SE TS)) % 4.63/4.88 (govtRepresentedBy DE a_2 a_1)) % 4.63/4.88 (narrativeSuccessor a_3 a_2 a_4)) % 4.63/4.88 (friendlyEvent a)) % 4.63/4.88 (govtRepresentedBy a a_4 a_5) → % 4.63/4.88 avoidTableSide a_5 a TS) % 4.63/4.88 True % 4.63/4.88 Clause #138 (by clausification #[137]): ∀ (a a_1 : event) (a_2 : person) (a_3 : govt) (a_4 : constrCont) (a_5 : govt) (a_6 : person), % 4.63/4.88 Eq % 4.63/4.88 (∀ (SE : event) (TS : table_side), % 4.63/4.88 And % 4.63/4.88 (And % 4.63/4.88 (And % 4.63/4.88 (And % 4.63/4.88 (And % 4.63/4.88 (And % 4.63/4.88 (And (And (And (pastColocatedDiplomaticEvent a a_1) (contentiousEvent a_1)) (subEvents a_1 SE)) % 4.63/4.89 (seatingEvent SE)) % 4.63/4.89 (performedBy SE a_2)) % 4.63/4.89 (seatedAtSide SE TS)) % 4.63/4.89 (govtRepresentedBy a_1 a_3 a_2)) % 4.63/4.89 (narrativeSuccessor a_4 a_3 a_5)) % 4.63/4.89 (friendlyEvent a)) % 4.63/4.89 (govtRepresentedBy a a_5 a_6) → % 4.63/4.89 avoidTableSide a_6 a TS) % 4.63/4.89 True % 4.63/4.89 Clause #139 (by clausification #[138]): ∀ (a a_1 a_2 : event) (a_3 : person) (a_4 : govt) (a_5 : constrCont) (a_6 : govt) (a_7 : person), % 4.63/4.89 Eq % 4.63/4.89 (∀ (TS : table_side), % 4.63/4.89 And % 4.63/4.89 (And % 4.63/4.89 (And % 4.63/4.89 (And % 4.63/4.89 (And % 4.63/4.89 (And % 4.63/4.89 (And (And (And (pastColocatedDiplomaticEvent a a_1) (contentiousEvent a_1)) (subEvents a_1 a_2)) % 4.63/4.89 (seatingEvent a_2)) % 4.63/4.89 (performedBy a_2 a_3)) % 4.63/4.89 (seatedAtSide a_2 TS)) % 4.63/4.89 (govtRepresentedBy a_1 a_4 a_3)) % 4.63/4.89 (narrativeSuccessor a_5 a_4 a_6)) % 4.63/4.89 (friendlyEvent a)) % 4.63/4.89 (govtRepresentedBy a a_6 a_7) → % 4.63/4.89 avoidTableSide a_7 a TS) % 4.63/4.89 True % 4.63/4.89 Clause #140 (by clausification #[139]): ∀ (a a_1 a_2 : event) (a_3 : person) (a_4 : table_side) (a_5 : govt) (a_6 : constrCont) (a_7 : govt) (a_8 : person), % 4.63/4.89 Eq % 4.63/4.89 (And % 4.63/4.89 (And % 4.63/4.89 (And % 4.63/4.89 (And % 4.63/4.89 (And % 4.63/4.89 (And % 4.63/4.89 (And (And (And (pastColocatedDiplomaticEvent a a_1) (contentiousEvent a_1)) (subEvents a_1 a_2)) % 4.63/4.89 (seatingEvent a_2)) % 4.63/4.89 (performedBy a_2 a_3)) % 4.63/4.89 (seatedAtSide a_2 a_4)) % 4.63/4.89 (govtRepresentedBy a_1 a_5 a_3)) % 4.63/4.89 (narrativeSuccessor a_6 a_5 a_7)) % 4.63/4.89 (friendlyEvent a)) % 4.63/4.89 (govtRepresentedBy a a_7 a_8) → % 4.63/4.89 avoidTableSide a_8 a a_4) % 4.63/4.89 True % 4.63/4.89 Clause #141 (by clausification #[140]): ∀ (a a_1 a_2 : event) (a_3 : person) (a_4 : table_side) (a_5 : govt) (a_6 : constrCont) (a_7 : govt) (a_8 : person), % 4.63/4.89 Or % 4.63/4.89 (Eq % 4.63/4.89 (And % 4.63/4.89 (And % 4.63/4.89 (And % 4.63/4.89 (And % 4.63/4.89 (And % 4.63/4.89 (And % 4.63/4.89 (And (And (And (pastColocatedDiplomaticEvent a a_1) (contentiousEvent a_1)) (subEvents a_1 a_2)) % 4.63/4.89 (seatingEvent a_2)) % 4.63/4.89 (performedBy a_2 a_3)) % 4.63/4.89 (seatedAtSide a_2 a_4)) % 4.63/4.89 (govtRepresentedBy a_1 a_5 a_3)) % 4.63/4.89 (narrativeSuccessor a_6 a_5 a_7)) % 4.63/4.89 (friendlyEvent a)) % 4.63/4.89 (govtRepresentedBy a a_7 a_8)) % 4.63/4.89 False) % 4.63/4.89 (Eq (avoidTableSide a_8 a a_4) True) % 4.63/4.89 Clause #142 (by clausification #[141]): ∀ (a : person) (a_1 : event) (a_2 : table_side) (a_3 a_4 : event) (a_5 : person) (a_6 : govt) (a_7 : constrCont) % 4.63/4.89 (a_8 : govt), % 4.63/4.89 Or (Eq (avoidTableSide a a_1 a_2) True) % 4.63/4.89 (Or % 4.63/4.89 (Eq % 4.63/4.89 (And % 4.63/4.89 (And % 4.63/4.89 (And % 4.63/4.89 (And % 4.63/4.89 (And % 4.63/4.89 (And (And (And (pastColocatedDiplomaticEvent a_1 a_3) (contentiousEvent a_3)) (subEvents a_3 a_4)) % 4.63/4.89 (seatingEvent a_4)) % 4.63/4.89 (performedBy a_4 a_5)) % 4.63/4.89 (seatedAtSide a_4 a_2)) % 4.63/4.89 (govtRepresentedBy a_3 a_6 a_5)) % 4.63/4.89 (narrativeSuccessor a_7 a_6 a_8)) % 4.63/4.89 (friendlyEvent a_1)) % 4.63/4.89 False) % 4.63/4.89 (Eq (govtRepresentedBy a_1 a_8 a) False)) % 4.63/4.89 Clause #143 (by clausification #[142]): ∀ (a : person) (a_1 : event) (a_2 : table_side) (a_3 : govt) (a_4 a_5 : event) (a_6 : person) (a_7 : govt) % 4.63/4.89 (a_8 : constrCont), % 4.63/4.89 Or (Eq (avoidTableSide a a_1 a_2) True) % 4.63/4.89 (Or (Eq (govtRepresentedBy a_1 a_3 a) False) % 4.63/4.89 (Or % 4.63/4.89 (Eq % 4.63/4.89 (And % 4.63/4.89 (And % 4.63/4.89 (And % 4.63/4.89 (And % 4.63/4.89 (And (And (And (pastColocatedDiplomaticEvent a_1 a_4) (contentiousEvent a_4)) (subEvents a_4 a_5)) % 4.63/4.89 (seatingEvent a_5)) % 4.63/4.89 (performedBy a_5 a_6)) % 4.63/4.89 (seatedAtSide a_5 a_2)) % 4.63/4.89 (govtRepresentedBy a_4 a_7 a_6)) % 4.63/4.89 (narrativeSuccessor a_8 a_7 a_3)) % 4.63/4.89 False) % 4.63/4.89 (Eq (friendlyEvent a_1) False))) % 4.63/4.89 Clause #144 (by clausification #[143]): ∀ (a : person) (a_1 : event) (a_2 : table_side) (a_3 : govt) (a_4 a_5 : event) (a_6 : person) (a_7 : govt) % 4.73/4.90 (a_8 : constrCont), % 4.73/4.90 Or (Eq (avoidTableSide a a_1 a_2) True) % 4.73/4.90 (Or (Eq (govtRepresentedBy a_1 a_3 a) False) % 4.73/4.90 (Or (Eq (friendlyEvent a_1) False) % 4.73/4.90 (Or % 4.73/4.90 (Eq % 4.73/4.90 (And % 4.73/4.90 (And % 4.73/4.90 (And % 4.73/4.90 (And (And (And (pastColocatedDiplomaticEvent a_1 a_4) (contentiousEvent a_4)) (subEvents a_4 a_5)) % 4.73/4.90 (seatingEvent a_5)) % 4.73/4.90 (performedBy a_5 a_6)) % 4.73/4.90 (seatedAtSide a_5 a_2)) % 4.73/4.90 (govtRepresentedBy a_4 a_7 a_6)) % 4.73/4.90 False) % 4.73/4.90 (Eq (narrativeSuccessor a_8 a_7 a_3) False)))) % 4.73/4.90 Clause #145 (by clausification #[144]): ∀ (a : person) (a_1 : event) (a_2 : table_side) (a_3 : govt) (a_4 : constrCont) (a_5 : govt) (a_6 a_7 : event) % 4.73/4.90 (a_8 : person), % 4.73/4.90 Or (Eq (avoidTableSide a a_1 a_2) True) % 4.73/4.90 (Or (Eq (govtRepresentedBy a_1 a_3 a) False) % 4.73/4.90 (Or (Eq (friendlyEvent a_1) False) % 4.73/4.90 (Or (Eq (narrativeSuccessor a_4 a_5 a_3) False) % 4.73/4.90 (Or % 4.73/4.90 (Eq % 4.73/4.90 (And % 4.73/4.90 (And % 4.73/4.90 (And (And (And (pastColocatedDiplomaticEvent a_1 a_6) (contentiousEvent a_6)) (subEvents a_6 a_7)) % 4.73/4.90 (seatingEvent a_7)) % 4.73/4.90 (performedBy a_7 a_8)) % 4.73/4.90 (seatedAtSide a_7 a_2)) % 4.73/4.90 False) % 4.73/4.90 (Eq (govtRepresentedBy a_6 a_5 a_8) False))))) % 4.73/4.90 Clause #146 (by clausification #[145]): ∀ (a : person) (a_1 : event) (a_2 : table_side) (a_3 : govt) (a_4 : constrCont) (a_5 : govt) (a_6 : event) % 4.73/4.90 (a_7 : person) (a_8 : event), % 4.73/4.90 Or (Eq (avoidTableSide a a_1 a_2) True) % 4.73/4.90 (Or (Eq (govtRepresentedBy a_1 a_3 a) False) % 4.73/4.90 (Or (Eq (friendlyEvent a_1) False) % 4.73/4.90 (Or (Eq (narrativeSuccessor a_4 a_5 a_3) False) % 4.73/4.90 (Or (Eq (govtRepresentedBy a_6 a_5 a_7) False) % 4.73/4.90 (Or % 4.73/4.90 (Eq % 4.73/4.90 (And % 4.73/4.90 (And (And (And (pastColocatedDiplomaticEvent a_1 a_6) (contentiousEvent a_6)) (subEvents a_6 a_8)) % 4.73/4.90 (seatingEvent a_8)) % 4.73/4.90 (performedBy a_8 a_7)) % 4.73/4.90 False) % 4.73/4.90 (Eq (seatedAtSide a_8 a_2) False)))))) % 4.73/4.90 Clause #147 (by clausification #[146]): ∀ (a : person) (a_1 : event) (a_2 : table_side) (a_3 : govt) (a_4 : constrCont) (a_5 : govt) (a_6 : event) % 4.73/4.90 (a_7 : person) (a_8 : event), % 4.73/4.90 Or (Eq (avoidTableSide a a_1 a_2) True) % 4.73/4.90 (Or (Eq (govtRepresentedBy a_1 a_3 a) False) % 4.73/4.90 (Or (Eq (friendlyEvent a_1) False) % 4.73/4.90 (Or (Eq (narrativeSuccessor a_4 a_5 a_3) False) % 4.73/4.90 (Or (Eq (govtRepresentedBy a_6 a_5 a_7) False) % 4.73/4.90 (Or (Eq (seatedAtSide a_8 a_2) False) % 4.73/4.90 (Or % 4.73/4.90 (Eq % 4.73/4.90 (And (And (And (pastColocatedDiplomaticEvent a_1 a_6) (contentiousEvent a_6)) (subEvents a_6 a_8)) % 4.73/4.90 (seatingEvent a_8)) % 4.73/4.90 False) % 4.73/4.90 (Eq (performedBy a_8 a_7) False))))))) % 4.73/4.90 Clause #148 (by clausification #[147]): ∀ (a : person) (a_1 : event) (a_2 : table_side) (a_3 : govt) (a_4 : constrCont) (a_5 : govt) (a_6 : event) % 4.73/4.90 (a_7 : person) (a_8 : event), % 4.73/4.90 Or (Eq (avoidTableSide a a_1 a_2) True) % 4.73/4.90 (Or (Eq (govtRepresentedBy a_1 a_3 a) False) % 4.73/4.90 (Or (Eq (friendlyEvent a_1) False) % 4.73/4.90 (Or (Eq (narrativeSuccessor a_4 a_5 a_3) False) % 4.73/4.90 (Or (Eq (govtRepresentedBy a_6 a_5 a_7) False) % 4.73/4.90 (Or (Eq (seatedAtSide a_8 a_2) False) % 4.73/4.90 (Or (Eq (performedBy a_8 a_7) False) % 4.73/4.90 (Or % 4.73/4.90 (Eq (And (And (pastColocatedDiplomaticEvent a_1 a_6) (contentiousEvent a_6)) (subEvents a_6 a_8)) % 4.73/4.90 False) % 4.73/4.90 (Eq (seatingEvent a_8) False)))))))) % 4.73/4.90 Clause #149 (by clausification #[148]): ∀ (a : person) (a_1 : event) (a_2 : table_side) (a_3 : govt) (a_4 : constrCont) (a_5 : govt) (a_6 : event) % 4.73/4.90 (a_7 : person) (a_8 : event), % 4.73/4.90 Or (Eq (avoidTableSide a a_1 a_2) True) % 4.73/4.90 (Or (Eq (govtRepresentedBy a_1 a_3 a) False) % 4.73/4.90 (Or (Eq (friendlyEvent a_1) False) % 4.73/4.90 (Or (Eq (narrativeSuccessor a_4 a_5 a_3) False) % 4.73/4.90 (Or (Eq (govtRepresentedBy a_6 a_5 a_7) False) % 4.73/4.90 (Or (Eq (seatedAtSide a_8 a_2) False) % 4.73/4.92 (Or (Eq (performedBy a_8 a_7) False) % 4.73/4.92 (Or (Eq (seatingEvent a_8) False) % 4.73/4.92 (Or (Eq (And (pastColocatedDiplomaticEvent a_1 a_6) (contentiousEvent a_6)) False) % 4.73/4.92 (Eq (subEvents a_6 a_8) False))))))))) % 4.73/4.92 Clause #150 (by clausification #[149]): ∀ (a : person) (a_1 : event) (a_2 : table_side) (a_3 : govt) (a_4 : constrCont) (a_5 : govt) (a_6 : event) % 4.73/4.92 (a_7 : person) (a_8 : event), % 4.73/4.92 Or (Eq (avoidTableSide a a_1 a_2) True) % 4.73/4.92 (Or (Eq (govtRepresentedBy a_1 a_3 a) False) % 4.73/4.92 (Or (Eq (friendlyEvent a_1) False) % 4.73/4.92 (Or (Eq (narrativeSuccessor a_4 a_5 a_3) False) % 4.73/4.92 (Or (Eq (govtRepresentedBy a_6 a_5 a_7) False) % 4.73/4.92 (Or (Eq (seatedAtSide a_8 a_2) False) % 4.73/4.92 (Or (Eq (performedBy a_8 a_7) False) % 4.73/4.92 (Or (Eq (seatingEvent a_8) False) % 4.73/4.92 (Or (Eq (subEvents a_6 a_8) False) % 4.73/4.92 (Or (Eq (pastColocatedDiplomaticEvent a_1 a_6) False) (Eq (contentiousEvent a_6) False)))))))))) % 4.73/4.92 Clause #156 (by superposition #[150, 50]): ∀ (a : table_side) (a_1 : constrCont) (a_2 : govt) (a_3 : event) (a_4 : person) (a_5 : event), % 4.73/4.92 Or (Eq (avoidTableSide merkel compiegneVisit2018 a) True) % 4.73/4.92 (Or (Eq (friendlyEvent compiegneVisit2018) False) % 4.73/4.92 (Or (Eq (narrativeSuccessor a_1 a_2 federalGermanRepublic) False) % 4.73/4.92 (Or (Eq (govtRepresentedBy a_3 a_2 a_4) False) % 4.73/4.92 (Or (Eq (seatedAtSide a_5 a) False) % 4.73/4.92 (Or (Eq (performedBy a_5 a_4) False) % 4.73/4.92 (Or (Eq (seatingEvent a_5) False) % 4.73/4.92 (Or (Eq (subEvents a_3 a_5) False) % 4.73/4.92 (Or (Eq (pastColocatedDiplomaticEvent compiegneVisit2018 a_3) False) % 4.73/4.92 (Or (Eq (contentiousEvent a_3) False) (Eq False True)))))))))) % 4.73/4.92 Clause #157 (by clausification #[131]): Eq (eventOccursAt compiegneVisit2018 france) True % 4.73/4.92 Clause #167 (by clausification #[82]): ∀ (a : geographicalRegion), Or (Eq (subRegions france a) True) (Eq (subRegions hautsDeFrance a) False) % 4.73/4.92 Clause #173 (by clausification #[83]): ∀ (a : geographicalRegion), Or (Eq (subRegions hautsDeFrance a) True) (Eq (subRegions picardy a) False) % 4.73/4.92 Clause #174 (by superposition #[173, 7]): Or (Eq (subRegions hautsDeFrance rethondesCompiegne) True) (Eq False True) % 4.73/4.92 Clause #175 (by clausification #[91]): ∀ (a : geographicalRegion), Or (Eq (eventOccursAt armistice1940 a) True) (Eq (subRegions a rethondesCompiegne) False) % 4.73/4.92 Clause #179 (by clausification #[174]): Eq (subRegions hautsDeFrance rethondesCompiegne) True % 4.73/4.92 Clause #182 (by superposition #[179, 167]): Or (Eq (subRegions france rethondesCompiegne) True) (Eq True False) % 4.73/4.92 Clause #184 (by clausification #[182]): Eq (subRegions france rethondesCompiegne) True % 4.73/4.92 Clause #185 (by superposition #[184, 175]): Or (Eq (eventOccursAt armistice1940 france) True) (Eq True False) % 4.73/4.92 Clause #187 (by clausification #[185]): Eq (eventOccursAt armistice1940 france) True % 4.73/4.92 Clause #226 (by clausification #[103]): ∀ (a : govt), % 4.73/4.92 Or (Eq (narrativeSuccessor germania thirdReich a) True) % 4.73/4.92 (Eq (narrativeSuccessor germania alliedOccupiedGermany a) False) % 4.73/4.92 Clause #227 (by superposition #[226, 14]): Or (Eq (narrativeSuccessor germania thirdReich federalGermanRepublic) True) (Eq False True) % 4.73/4.92 Clause #228 (by clausification #[227]): Eq (narrativeSuccessor germania thirdReich federalGermanRepublic) True % 4.73/4.92 Clause #270 (by clausification #[120]): ∀ (a : geographicalRegion), % 4.73/4.92 Or (Eq (pastColocatedDiplomaticEvent compiegneVisit2018 armistice1940) True) % 4.73/4.92 (Or (Eq (eventOccursAt compiegneVisit2018 a) False) % 4.73/4.92 (Or (Eq (diplomaticEvent armistice1940) False) (Eq (eventOccursAt armistice1940 a) False))) % 4.73/4.92 Clause #271 (by forward demodulation #[270, 105]): ∀ (a : geographicalRegion), % 4.73/4.92 Or (Eq (pastColocatedDiplomaticEvent compiegneVisit2018 armistice1940) True) % 4.73/4.92 (Or (Eq (eventOccursAt compiegneVisit2018 a) False) (Or (Eq True False) (Eq (eventOccursAt armistice1940 a) False))) % 4.73/4.92 Clause #272 (by clausification #[271]): ∀ (a : geographicalRegion), % 4.73/4.92 Or (Eq (pastColocatedDiplomaticEvent compiegneVisit2018 armistice1940) True) % 4.73/4.92 (Or (Eq (eventOccursAt compiegneVisit2018 a) False) (Eq (eventOccursAt armistice1940 a) False)) % 4.73/4.94 Clause #276 (by superposition #[272, 157]): Or (Eq (pastColocatedDiplomaticEvent compiegneVisit2018 armistice1940) True) % 4.73/4.94 (Or (Eq (eventOccursAt armistice1940 france) False) (Eq False True)) % 4.73/4.94 Clause #277 (by clausification #[276]): Or (Eq (pastColocatedDiplomaticEvent compiegneVisit2018 armistice1940) True) % 4.73/4.94 (Eq (eventOccursAt armistice1940 france) False) % 4.73/4.94 Clause #278 (by forward demodulation #[277, 187]): Or (Eq (pastColocatedDiplomaticEvent compiegneVisit2018 armistice1940) True) (Eq True False) % 4.73/4.94 Clause #279 (by clausification #[278]): Eq (pastColocatedDiplomaticEvent compiegneVisit2018 armistice1940) True % 4.73/4.94 Clause #299 (by clausification #[156]): ∀ (a : table_side) (a_1 : constrCont) (a_2 : govt) (a_3 : event) (a_4 : person) (a_5 : event), % 4.73/4.94 Or (Eq (avoidTableSide merkel compiegneVisit2018 a) True) % 4.73/4.94 (Or (Eq (friendlyEvent compiegneVisit2018) False) % 4.73/4.94 (Or (Eq (narrativeSuccessor a_1 a_2 federalGermanRepublic) False) % 4.73/4.94 (Or (Eq (govtRepresentedBy a_3 a_2 a_4) False) % 4.73/4.94 (Or (Eq (seatedAtSide a_5 a) False) % 4.73/4.94 (Or (Eq (performedBy a_5 a_4) False) % 4.73/4.94 (Or (Eq (seatingEvent a_5) False) % 4.73/4.94 (Or (Eq (subEvents a_3 a_5) False) % 4.73/4.94 (Or (Eq (pastColocatedDiplomaticEvent compiegneVisit2018 a_3) False) % 4.73/4.94 (Eq (contentiousEvent a_3) False))))))))) % 4.73/4.94 Clause #300 (by forward demodulation #[299, 49]): ∀ (a : table_side) (a_1 : constrCont) (a_2 : govt) (a_3 : event) (a_4 : person) (a_5 : event), % 4.73/4.94 Or (Eq (avoidTableSide merkel compiegneVisit2018 a) True) % 4.73/4.94 (Or (Eq True False) % 4.73/4.94 (Or (Eq (narrativeSuccessor a_1 a_2 federalGermanRepublic) False) % 4.73/4.94 (Or (Eq (govtRepresentedBy a_3 a_2 a_4) False) % 4.73/4.94 (Or (Eq (seatedAtSide a_5 a) False) % 4.73/4.94 (Or (Eq (performedBy a_5 a_4) False) % 4.73/4.94 (Or (Eq (seatingEvent a_5) False) % 4.73/4.94 (Or (Eq (subEvents a_3 a_5) False) % 4.73/4.94 (Or (Eq (pastColocatedDiplomaticEvent compiegneVisit2018 a_3) False) % 4.73/4.94 (Eq (contentiousEvent a_3) False))))))))) % 4.73/4.94 Clause #301 (by clausification #[300]): ∀ (a : table_side) (a_1 : constrCont) (a_2 : govt) (a_3 : event) (a_4 : person) (a_5 : event), % 4.73/4.94 Or (Eq (avoidTableSide merkel compiegneVisit2018 a) True) % 4.73/4.94 (Or (Eq (narrativeSuccessor a_1 a_2 federalGermanRepublic) False) % 4.73/4.94 (Or (Eq (govtRepresentedBy a_3 a_2 a_4) False) % 4.73/4.94 (Or (Eq (seatedAtSide a_5 a) False) % 4.73/4.94 (Or (Eq (performedBy a_5 a_4) False) % 4.73/4.94 (Or (Eq (seatingEvent a_5) False) % 4.73/4.94 (Or (Eq (subEvents a_3 a_5) False) % 4.73/4.94 (Or (Eq (pastColocatedDiplomaticEvent compiegneVisit2018 a_3) False) % 4.73/4.94 (Eq (contentiousEvent a_3) False)))))))) % 4.73/4.94 Clause #303 (by superposition #[301, 228]): ∀ (a : table_side) (a_1 : event) (a_2 : person) (a_3 : event), % 4.73/4.94 Or (Eq (avoidTableSide merkel compiegneVisit2018 a) True) % 4.73/4.94 (Or (Eq (govtRepresentedBy a_1 thirdReich a_2) False) % 4.73/4.94 (Or (Eq (seatedAtSide a_3 a) False) % 4.73/4.94 (Or (Eq (performedBy a_3 a_2) False) % 4.73/4.94 (Or (Eq (seatingEvent a_3) False) % 4.73/4.94 (Or (Eq (subEvents a_1 a_3) False) % 4.73/4.94 (Or (Eq (pastColocatedDiplomaticEvent compiegneVisit2018 a_1) False) % 4.73/4.94 (Or (Eq (contentiousEvent a_1) False) (Eq False True)))))))) % 4.73/4.94 Clause #337 (by clausification #[303]): ∀ (a : table_side) (a_1 : event) (a_2 : person) (a_3 : event), % 4.73/4.94 Or (Eq (avoidTableSide merkel compiegneVisit2018 a) True) % 4.73/4.94 (Or (Eq (govtRepresentedBy a_1 thirdReich a_2) False) % 4.73/4.94 (Or (Eq (seatedAtSide a_3 a) False) % 4.73/4.94 (Or (Eq (performedBy a_3 a_2) False) % 4.73/4.94 (Or (Eq (seatingEvent a_3) False) % 4.73/4.94 (Or (Eq (subEvents a_1 a_3) False) % 4.73/4.94 (Or (Eq (pastColocatedDiplomaticEvent compiegneVisit2018 a_1) False) % 4.73/4.94 (Eq (contentiousEvent a_1) False))))))) % 4.73/4.94 Clause #338 (by superposition #[337, 35]): ∀ (a : table_side) (a_1 : event), % 4.73/4.94 Or (Eq (avoidTableSide merkel compiegneVisit2018 a) True) % 4.73/4.94 (Or (Eq (seatedAtSide a_1 a) False) % 4.73/4.94 (Or (Eq (performedBy a_1 hitler) False) % 4.73/4.94 (Or (Eq (seatingEvent a_1) False) % 4.73/4.95 (Or (Eq (subEvents armistice1940 a_1) False) % 4.73/4.95 (Or (Eq (pastColocatedDiplomaticEvent compiegneVisit2018 armistice1940) False) % 4.73/4.95 (Or (Eq (contentiousEvent armistice1940) False) (Eq False True))))))) % 4.73/4.95 Clause #339 (by clausification #[338]): ∀ (a : table_side) (a_1 : event), % 4.73/4.95 Or (Eq (avoidTableSide merkel compiegneVisit2018 a) True) % 4.73/4.95 (Or (Eq (seatedAtSide a_1 a) False) % 4.73/4.95 (Or (Eq (performedBy a_1 hitler) False) % 4.73/4.95 (Or (Eq (seatingEvent a_1) False) % 4.73/4.95 (Or (Eq (subEvents armistice1940 a_1) False) % 4.73/4.95 (Or (Eq (pastColocatedDiplomaticEvent compiegneVisit2018 armistice1940) False) % 4.73/4.95 (Eq (contentiousEvent armistice1940) False)))))) % 4.73/4.95 Clause #340 (by forward demodulation #[339, 279]): ∀ (a : table_side) (a_1 : event), % 4.73/4.95 Or (Eq (avoidTableSide merkel compiegneVisit2018 a) True) % 4.73/4.95 (Or (Eq (seatedAtSide a_1 a) False) % 4.73/4.95 (Or (Eq (performedBy a_1 hitler) False) % 4.73/4.95 (Or (Eq (seatingEvent a_1) False) % 4.73/4.95 (Or (Eq (subEvents armistice1940 a_1) False) % 4.73/4.95 (Or (Eq True False) (Eq (contentiousEvent armistice1940) False)))))) % 4.73/4.95 Clause #341 (by clausification #[340]): ∀ (a : table_side) (a_1 : event), % 4.73/4.95 Or (Eq (avoidTableSide merkel compiegneVisit2018 a) True) % 4.73/4.95 (Or (Eq (seatedAtSide a_1 a) False) % 4.73/4.95 (Or (Eq (performedBy a_1 hitler) False) % 4.73/4.95 (Or (Eq (seatingEvent a_1) False) % 4.73/4.95 (Or (Eq (subEvents armistice1940 a_1) False) (Eq (contentiousEvent armistice1940) False))))) % 4.73/4.95 Clause #342 (by forward demodulation #[341, 108]): ∀ (a : table_side) (a_1 : event), % 4.73/4.95 Or (Eq (avoidTableSide merkel compiegneVisit2018 a) True) % 4.73/4.95 (Or (Eq (seatedAtSide a_1 a) False) % 4.73/4.95 (Or (Eq (performedBy a_1 hitler) False) % 4.73/4.95 (Or (Eq (seatingEvent a_1) False) (Or (Eq (subEvents armistice1940 a_1) False) (Eq True False))))) % 4.73/4.95 Clause #343 (by clausification #[342]): ∀ (a : table_side) (a_1 : event), % 4.73/4.95 Or (Eq (avoidTableSide merkel compiegneVisit2018 a) True) % 4.73/4.95 (Or (Eq (seatedAtSide a_1 a) False) % 4.73/4.95 (Or (Eq (performedBy a_1 hitler) False) % 4.73/4.95 (Or (Eq (seatingEvent a_1) False) (Eq (subEvents armistice1940 a_1) False)))) % 4.73/4.95 Clause #347 (by superposition #[343, 40]): Or (Eq (avoidTableSide merkel compiegneVisit2018 cwlTableSideA) True) % 4.73/4.95 (Or (Eq (performedBy armistice1940GermanSeating hitler) False) % 4.73/4.95 (Or (Eq (seatingEvent armistice1940GermanSeating) False) % 4.73/4.95 (Or (Eq (subEvents armistice1940 armistice1940GermanSeating) False) (Eq False True)))) % 4.73/4.95 Clause #349 (by clausification #[347]): Or (Eq (avoidTableSide merkel compiegneVisit2018 cwlTableSideA) True) % 4.73/4.95 (Or (Eq (performedBy armistice1940GermanSeating hitler) False) % 4.73/4.95 (Or (Eq (seatingEvent armistice1940GermanSeating) False) % 4.73/4.95 (Eq (subEvents armistice1940 armistice1940GermanSeating) False))) % 4.73/4.95 Clause #350 (by forward demodulation #[349, 39]): Or (Eq (avoidTableSide merkel compiegneVisit2018 cwlTableSideA) True) % 4.73/4.95 (Or (Eq True False) % 4.73/4.95 (Or (Eq (seatingEvent armistice1940GermanSeating) False) % 4.73/4.95 (Eq (subEvents armistice1940 armistice1940GermanSeating) False))) % 4.73/4.95 Clause #351 (by clausification #[350]): Or (Eq (avoidTableSide merkel compiegneVisit2018 cwlTableSideA) True) % 4.73/4.95 (Or (Eq (seatingEvent armistice1940GermanSeating) False) % 4.73/4.95 (Eq (subEvents armistice1940 armistice1940GermanSeating) False)) % 4.73/4.95 Clause #352 (by forward demodulation #[351, 37]): Or (Eq (avoidTableSide merkel compiegneVisit2018 cwlTableSideA) True) % 4.73/4.95 (Or (Eq True False) (Eq (subEvents armistice1940 armistice1940GermanSeating) False)) % 4.73/4.95 Clause #353 (by clausification #[352]): Or (Eq (avoidTableSide merkel compiegneVisit2018 cwlTableSideA) True) % 4.73/4.95 (Eq (subEvents armistice1940 armistice1940GermanSeating) False) % 4.73/4.95 Clause #354 (by forward demodulation #[353, 38]): Or (Eq (avoidTableSide merkel compiegneVisit2018 cwlTableSideA) True) (Eq True False) % 4.73/4.95 Clause #355 (by clausification #[354]): Eq (avoidTableSide merkel compiegneVisit2018 cwlTableSideA) True % 4.73/4.95 Clause #356 (by superposition #[355, 112]): Eq True False % 4.73/4.95 Clause #357 (by clausification #[356]): False % 4.73/4.95 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------