%------------------------------------------------------------------------------ % File : SPASS+T---2.2.22 % Problem : PUZ012_1 : TPTP v8.1.0. Released v5.0.0. % Transfm : none % Format : tptp:raw % Command : spasst-tptp-script %s %d % Computer : n029.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 : Mon Jul 18 18:27:35 EDT 2022 % Result : Theorem 0.41s 1.02s % Output : Refutation 0.41s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.09/0.11 % Problem : PUZ012_1 : TPTP v8.1.0. Released v5.0.0. % 0.09/0.12 % Command : spasst-tptp-script %s %d % 0.12/0.32 % Computer : n029.cluster.edu % 0.12/0.32 % Model : x86_64 x86_64 % 0.12/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.32 % Memory : 8042.1875MB % 0.12/0.32 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.32 % CPULimit : 300 % 0.12/0.32 % WCLimit : 600 % 0.12/0.32 % DateTime : Sat May 28 22:48:58 EDT 2022 % 0.12/0.33 % CPUTime : % 0.18/0.45 % Using EUF theory % 0.41/1.02 % 0.41/1.02 % 0.41/1.02 % SZS status Theorem for /tmp/SPASST_5168_n029.cluster.edu % 0.41/1.02 % 0.41/1.02 SPASS V 2.2.22 in combination with yices. % 0.41/1.02 SPASS beiseite: Proof found by SPASS. % 0.41/1.02 Problem: /tmp/SPASST_5168_n029.cluster.edu % 0.41/1.02 SPASS derived 38 clauses, backtracked 10 clauses and kept 68 clauses. % 0.41/1.02 SPASS backtracked 3 times (0 times due to theory inconsistency). % 0.41/1.02 SPASS allocated 6360 KBytes. % 0.41/1.02 SPASS spent 0:00:00.01 on the problem. % 0.41/1.02 0:00:00.00 for the input. % 0.41/1.02 0:00:00.00 for the FLOTTER CNF translation. % 0.41/1.02 0:00:00.00 for inferences. % 0.41/1.02 0:00:00.00 for the backtracking. % 0.41/1.02 0:00:00.00 for the reduction. % 0.41/1.02 0:00:00.00 for interacting with the SMT procedure. % 0.41/1.02 % 0.41/1.02 % 0.41/1.02 % SZS output start CNFRefutation for /tmp/SPASST_5168_n029.cluster.edu % 0.41/1.02 % 0.41/1.02 % Here is a proof with depth 4, length 39 : % 0.41/1.02 1[0:Inp] || -> fruit(oranges)*. % 0.41/1.02 2[0:Inp] || -> fruit(bananas)*. % 0.41/1.02 3[0:Inp] || -> fruit(apples)*. % 0.41/1.02 4[0:Inp] || -> box_p(boxc)*. % 0.41/1.02 5[0:Inp] || -> box_p(boxb)*. % 0.41/1.02 6[0:Inp] || -> box_p(boxa)*. % 0.41/1.02 9[0:Inp] || -> contains(boxb,apples)*. % 0.41/1.02 10[0:Inp] || -> label(boxc,bananas)*. % 0.41/1.02 11[0:Inp] || -> label(boxb,oranges)*. % 0.41/1.02 14[0:Inp] || equal_fruits(bananas,oranges)*+ -> . % 0.41/1.02 15[0:Inp] || equal_fruits(apples,bananas)*+ -> . % 0.41/1.02 21(e)[0:Inp] || contains(boxa,bananas)*+ contains(boxc,oranges) -> . % 0.41/1.02 23[0:Inp] || fruit(U)+ -> contains(boxa,U)* contains(boxb,U) contains(boxc,U). % 0.41/1.02 24[0:Inp] || box_p(U) fruit(V) label(U,V)+ contains(U,V)* -> . % 0.41/1.02 25[0:Inp] || box_p(U) fruit(V) fruit(W) contains(U,V)*+ contains(U,W)* -> equal_fruits(V,W)*. % 0.41/1.02 45(e)[0:Res:2.0,23.0] || -> contains(boxa,bananas)* contains(boxb,bananas) contains(boxc,bananas). % 0.41/1.02 46[0:Res:1.0,23.0] || -> contains(boxa,oranges)* contains(boxb,oranges) contains(boxc,oranges). % 0.41/1.02 47[1:Spt:45.0] || -> contains(boxa,bananas)*. % 0.41/1.02 48[1:MRR:21.0,47.0] || contains(boxc,oranges)*+ -> . % 0.41/1.02 49(e)[1:MRR:46.2,48.0] || -> contains(boxa,oranges)* contains(boxb,oranges). % 0.41/1.02 50[2:Spt:49.0] || -> contains(boxa,oranges)*. % 0.41/1.02 58[0:Res:11.0,24.2] || box_p(boxb) fruit(oranges) contains(boxb,oranges)* -> . % 0.41/1.02 59[0:Res:10.0,24.2] || box_p(boxc) fruit(bananas) contains(boxc,bananas)* -> . % 0.41/1.02 61[0:MRR:58.0,58.1,5.0,1.0] || contains(boxb,oranges)*+ -> . % 0.41/1.02 62[0:MRR:59.0,59.1,4.0,2.0] || contains(boxc,bananas)*+ -> . % 0.41/1.02 64[0:Res:9.0,25.3] || box_p(boxb) fruit(apples) fruit(U) contains(boxb,U) -> equal_fruits(apples,U)*. % 0.41/1.02 65[1:Res:47.0,25.3] || box_p(boxa) fruit(bananas) fruit(U) contains(boxa,U) -> equal_fruits(bananas,U)*. % 0.41/1.02 69[0:MRR:64.0,64.1,5.0,3.0] || fruit(U) contains(boxb,U)+ -> equal_fruits(apples,U)*. % 0.41/1.02 70[1:MRR:65.0,65.1,6.0,2.0] || fruit(U) contains(boxa,U)+ -> equal_fruits(bananas,U)*. % 0.41/1.02 79[2:Res:50.0,70.1] || fruit(oranges) -> equal_fruits(bananas,oranges)*. % 0.41/1.02 81(e)[2:MRR:79.0,79.1,1.0,14.0] || -> . % 0.41/1.02 83(e)[2:Spt:81.0,49.0,50.0] || contains(boxa,oranges)* -> . % 0.41/1.02 84[2:Spt:81.0,49.1] || -> contains(boxb,oranges)*. % 0.41/1.02 85(e)[2:MRR:84.0,61.0] || -> . % 0.41/1.02 86(e)[1:Spt:85.0,45.0,47.0] || contains(boxa,bananas)* -> . % 0.41/1.02 87[1:Spt:85.0,45.1,45.2] || -> contains(boxb,bananas)* contains(boxc,bananas). % 0.41/1.02 88[1:MRR:87.1,62.0] || -> contains(boxb,bananas)*. % 0.41/1.02 93[1:Res:88.0,69.1] || fruit(bananas) -> equal_fruits(apples,bananas)*. % 0.41/1.02 95(e)[1:MRR:93.0,93.1,2.0,15.0] || -> . % 0.41/1.02 % 0.41/1.02 % SZS output end CNFRefutation for /tmp/SPASST_5168_n029.cluster.edu % 0.41/1.02 % 0.41/1.02 Formulae used in the proof : fof_oranges_type fof_bananas_type fof_apples_type fof_boxc_type fof_boxb_type fof_boxa_type fof_boxb_contains_apples fof_boxc_labelled_bananas fof_boxb_labelled_oranges fof_bananas_not_oranges fof_apples_not_bananas fof_prove_boxa_contains_bananas_and_boxc_oranges fof_each_thing_is_in_a_box fof_label_is_wrong fof_contains_is_well_defined1 % 0.75/1.04 % 0.75/1.04 SPASS+T ended %------------------------------------------------------------------------------