%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : COL106-2 : TPTP v9.0.0. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% Computer : n031.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 : Wed Apr 9 05:48:05 PM UTC 2025
% Result : Unsatisfiable 5.26s 2.37s
% Output : CNFRefutation 5.60s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 12
% Syntax : Number of formulae : 72 ( 44 unt; 0 typ; 0 def)
% Number of atoms : 121 ( 70 equ)
% Maximal formula atoms : 5 ( 1 avg)
% Number of connectives : 85 ( 36 ~; 49 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 3 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-3 aty)
% Number of functors : 15 ( 15 usr; 7 con; 0-4 aty)
% Number of variables : 78 ( 78 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ c_in > c_Pair > v_sko__uTI > v_sko__uTH > v_sko__uTG > v_sko__uTF > v_sko__uTE > tc_prod > c_Comb_Ocomb_Oop_A_D_D > #nlpp > v_ya > v_xb > v_x > tc_Comb_Ocomb > c_Comb_Oparcontract > c_Comb_Ocomb_OS > c_Comb_Ocomb_OK
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(v_x,type,
v_x: $i ).
tff(v_sko__uTF,type,
v_sko__uTF: ( $i * $i * $i ) > $i ).
tff(v_sko__uTG,type,
v_sko__uTG: ( $i * $i * $i ) > $i ).
tff(c_Comb_Ocomb_OK,type,
c_Comb_Ocomb_OK: $i ).
tff(tc_prod,type,
tc_prod: ( $i * $i ) > $i ).
tff(v_ya,type,
v_ya: $i ).
tff(c_in,type,
c_in: ( $i * $i * $i ) > $o ).
tff(v_sko__uTI,type,
v_sko__uTI: ( $i * $i * $i ) > $i ).
tff(v_sko__uTE,type,
v_sko__uTE: ( $i * $i ) > $i ).
tff(c_Comb_Oparcontract,type,
c_Comb_Oparcontract: $i ).
tff(c_Comb_Ocomb_OS,type,
c_Comb_Ocomb_OS: $i ).
tff(c_Pair,type,
c_Pair: ( $i * $i * $i * $i ) > $i ).
tff(c_Comb_Ocomb_Oop_A_D_D,type,
c_Comb_Ocomb_Oop_A_D_D: ( $i * $i ) > $i ).
tff(v_sko__uTH,type,
v_sko__uTH: ( $i * $i * $i ) > $i ).
tff(tc_Comb_Ocomb,type,
tc_Comb_Ocomb: $i ).
tff(v_xb,type,
v_xb: $i ).
tff(f_57,axiom,
! [V_comb1_H,V_comb2_H] : ( c_Comb_Ocomb_OK != c_Comb_Ocomb_Oop_A_D_D(V_comb1_H,V_comb2_H) ),
file(unknown,unknown) ).
tff(f_79,axiom,
! [V_x] : c_in(c_Pair(V_x,V_x,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)),
file(unknown,unknown) ).
tff(f_81,axiom,
! [V_x,V_y] : c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,V_x),V_y),V_x,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)),
file(unknown,unknown) ).
tff(f_89,axiom,
! [V_z,V_w,V_x,V_y] :
( ~ c_in(c_Pair(V_z,V_w,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| ~ c_in(c_Pair(V_x,V_y,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(V_x,V_z),c_Comb_Ocomb_Oop_A_D_D(V_y,V_w),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)) ),
file(unknown,unknown) ).
tff(f_72,axiom,
! [V_x,V_z] :
( ~ c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,V_x),V_z,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| ( V_z = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_sko__uTE(V_x,V_z)) ) ),
file(unknown,unknown) ).
tff(f_67,axiom,
! [V_comb1,V_comb2,V_comb1_H,V_comb2_H] :
( ( c_Comb_Ocomb_Oop_A_D_D(V_comb1,V_comb2) != c_Comb_Ocomb_Oop_A_D_D(V_comb1_H,V_comb2_H) )
| ( V_comb2 = V_comb2_H ) ),
file(unknown,unknown) ).
tff(f_26,axiom,
c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya),v_xb,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)),
file(unknown,unknown) ).
tff(f_43,axiom,
! [V_p,V_q,V_r] :
( ~ c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(V_p,V_q),V_r,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| ( V_r = c_Comb_Ocomb_Oop_A_D_D(V_p,V_q) )
| ( V_p = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,V_r) )
| ( V_p = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTF(V_p,V_q,V_r)),v_sko__uTG(V_p,V_q,V_r)) )
| ( V_r = c_Comb_Ocomb_Oop_A_D_D(v_sko__uTI(V_p,V_q,V_r),v_sko__uTH(V_p,V_q,V_r)) ) ),
file(unknown,unknown) ).
tff(f_32,axiom,
! [V_U] :
( ~ c_in(c_Pair(v_xb,V_U,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| ~ c_in(c_Pair(v_x,V_U,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)) ),
file(unknown,unknown) ).
tff(f_54,axiom,
! [V_p,V_q,V_r] :
( ~ c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(V_p,V_q),V_r,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| c_in(c_Pair(V_p,v_sko__uTI(V_p,V_q,V_r),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| ( V_r = c_Comb_Ocomb_Oop_A_D_D(V_p,V_q) )
| ( V_p = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,V_r) )
| ( V_p = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTF(V_p,V_q,V_r)),v_sko__uTG(V_p,V_q,V_r)) ) ),
file(unknown,unknown) ).
tff(f_77,axiom,
! [V_x,V_z] :
( ~ c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,V_x),V_z,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| c_in(c_Pair(V_x,v_sko__uTE(V_x,V_z),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)) ),
file(unknown,unknown) ).
tff(f_62,axiom,
! [V_comb1,V_comb2,V_comb1_H,V_comb2_H] :
( ( c_Comb_Ocomb_Oop_A_D_D(V_comb1,V_comb2) != c_Comb_Ocomb_Oop_A_D_D(V_comb1_H,V_comb2_H) )
| ( V_comb1 = V_comb1_H ) ),
file(unknown,unknown) ).
tff(c_10,plain,
! [V_comb1_H_8,V_comb2_H_9] : ( c_Comb_Ocomb_Oop_A_D_D(V_comb1_H_8,V_comb2_H_9) != c_Comb_Ocomb_OK ),
inference(cnfTransformation,[status(thm)],[f_57]) ).
tff(c_20,plain,
! [V_x_22] : c_in(c_Pair(V_x_22,V_x_22,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)),
inference(cnfTransformation,[status(thm)],[f_79]) ).
tff(c_22,plain,
! [V_x_23,V_y_24] : c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,V_x_23),V_y_24),V_x_23,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)),
inference(cnfTransformation,[status(thm)],[f_81]) ).
tff(c_119,plain,
! [V_x_52,V_z_53,V_y_54,V_w_55] :
( c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(V_x_52,V_z_53),c_Comb_Ocomb_Oop_A_D_D(V_y_54,V_w_55),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| ~ c_in(c_Pair(V_x_52,V_y_54,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| ~ c_in(c_Pair(V_z_53,V_w_55,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)) ),
inference(cnfTransformation,[status(thm)],[f_89]) ).
tff(c_16,plain,
! [V_x_18,V_z_19] :
( ( c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_sko__uTE(V_x_18,V_z_19)) = V_z_19 )
| ~ c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,V_x_18),V_z_19,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)) ),
inference(cnfTransformation,[status(thm)],[f_72]) ).
tff(c_130,plain,
! [V_z_56,V_y_57,V_w_58] :
( ( c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_sko__uTE(V_z_56,c_Comb_Ocomb_Oop_A_D_D(V_y_57,V_w_58))) = c_Comb_Ocomb_Oop_A_D_D(V_y_57,V_w_58) )
| ~ c_in(c_Pair(c_Comb_Ocomb_OK,V_y_57,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| ~ c_in(c_Pair(V_z_56,V_w_58,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)) ),
inference(resolution,[status(thm)],[c_119,c_16]) ).
tff(c_135,plain,
! [V_z_59,V_w_60] :
( ( c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_sko__uTE(V_z_59,c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,V_w_60))) = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,V_w_60) )
| ~ c_in(c_Pair(V_z_59,V_w_60,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)) ),
inference(resolution,[status(thm)],[c_20,c_130]) ).
tff(c_153,plain,
! [V_x_61,V_y_62] : ( c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_sko__uTE(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,V_x_61),V_y_62),c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,V_x_61))) = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,V_x_61) ),
inference(resolution,[status(thm)],[c_22,c_135]) ).
tff(c_14,plain,
! [V_comb2_H_17,V_comb2_15,V_comb1_H_16,V_comb1_14] :
( ( V_comb2_H_17 = V_comb2_15 )
| ( c_Comb_Ocomb_Oop_A_D_D(V_comb1_H_16,V_comb2_H_17) != c_Comb_Ocomb_Oop_A_D_D(V_comb1_14,V_comb2_15) ) ),
inference(cnfTransformation,[status(thm)],[f_67]) ).
tff(c_191,plain,
! [V_x_61,V_y_62,V_comb2_H_17,V_comb1_H_16] :
( ( v_sko__uTE(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,V_x_61),V_y_62),c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,V_x_61)) = V_comb2_H_17 )
| ( c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,V_x_61) != c_Comb_Ocomb_Oop_A_D_D(V_comb1_H_16,V_comb2_H_17) ) ),
inference(superposition,[status(thm),theory(equality)],[c_153,c_14]) ).
tff(c_278,plain,
! [V_comb2_H_17,V_y_62] : ( v_sko__uTE(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,V_comb2_H_17),V_y_62),c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,V_comb2_H_17)) = V_comb2_H_17 ),
inference(reflexivity,[status(thm),theory(equality)],[c_191]) ).
tff(c_2,plain,
c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya),v_xb,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)),
inference(cnfTransformation,[status(thm)],[f_26]) ).
tff(c_252,plain,
! [V_p_63,V_q_64,V_r_65] :
( ( c_Comb_Ocomb_Oop_A_D_D(v_sko__uTI(V_p_63,V_q_64,V_r_65),v_sko__uTH(V_p_63,V_q_64,V_r_65)) = V_r_65 )
| ( c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTF(V_p_63,V_q_64,V_r_65)),v_sko__uTG(V_p_63,V_q_64,V_r_65)) = V_p_63 )
| ( c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,V_r_65) = V_p_63 )
| ( c_Comb_Ocomb_Oop_A_D_D(V_p_63,V_q_64) = V_r_65 )
| ~ c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(V_p_63,V_q_64),V_r_65,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)) ),
inference(cnfTransformation,[status(thm)],[f_43]) ).
tff(c_273,plain,
( ( c_Comb_Ocomb_Oop_A_D_D(v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb),v_sko__uTH(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb)) = v_xb )
| ( c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTF(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb)),v_sko__uTG(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb)) = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x) )
| ( c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_xb) = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x) )
| ( c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya) = v_xb ) ),
inference(resolution,[status(thm)],[c_2,c_252]) ).
tff(c_481,plain,
c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya) = v_xb,
inference(splitLeft,[status(thm)],[c_273]) ).
tff(c_514,plain,
c_in(c_Pair(v_xb,v_x,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)),
inference(superposition,[status(thm),theory(equality)],[c_481,c_22]) ).
tff(c_4,plain,
! [V_U_1] :
( ~ c_in(c_Pair(v_x,V_U_1,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| ~ c_in(c_Pair(v_xb,V_U_1,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)) ),
inference(cnfTransformation,[status(thm)],[f_32]) ).
tff(c_571,plain,
~ c_in(c_Pair(v_x,v_x,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)),
inference(resolution,[status(thm)],[c_514,c_4]) ).
tff(c_577,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_20,c_571]) ).
tff(c_579,plain,
c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya) != v_xb,
inference(splitRight,[status(thm)],[c_273]) ).
tff(c_314,plain,
! [V_p_72,V_q_73,V_r_74] :
( ( c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTF(V_p_72,V_q_73,V_r_74)),v_sko__uTG(V_p_72,V_q_73,V_r_74)) = V_p_72 )
| ( c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,V_r_74) = V_p_72 )
| ( c_Comb_Ocomb_Oop_A_D_D(V_p_72,V_q_73) = V_r_74 )
| c_in(c_Pair(V_p_72,v_sko__uTI(V_p_72,V_q_73,V_r_74),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| ~ c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(V_p_72,V_q_73),V_r_74,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)) ),
inference(cnfTransformation,[status(thm)],[f_54]) ).
tff(c_327,plain,
( ( c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTF(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb)),v_sko__uTG(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb)) = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x) )
| ( c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_xb) = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x) )
| ( c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya) = v_xb )
| c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)) ),
inference(resolution,[status(thm)],[c_2,c_314]) ).
tff(c_846,plain,
( ( c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTF(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb)),v_sko__uTG(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb)) = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x) )
| ( c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_xb) = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x) )
| c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)) ),
inference(negUnitSimplification,[status(thm)],[c_579,c_327]) ).
tff(c_847,plain,
c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)),
inference(splitLeft,[status(thm)],[c_846]) ).
tff(c_18,plain,
! [V_x_20,V_z_21] :
( c_in(c_Pair(V_x_20,v_sko__uTE(V_x_20,V_z_21),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| ~ c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,V_x_20),V_z_21,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)) ),
inference(cnfTransformation,[status(thm)],[f_77]) ).
tff(c_867,plain,
c_in(c_Pair(v_x,v_sko__uTE(v_x,v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb)),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)),
inference(resolution,[status(thm)],[c_847,c_18]) ).
tff(c_578,plain,
( ( c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_xb) = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x) )
| ( c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTF(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb)),v_sko__uTG(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb)) = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x) )
| ( c_Comb_Ocomb_Oop_A_D_D(v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb),v_sko__uTH(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb)) = v_xb ) ),
inference(splitRight,[status(thm)],[c_273]) ).
tff(c_580,plain,
c_Comb_Ocomb_Oop_A_D_D(v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb),v_sko__uTH(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb)) = v_xb,
inference(splitLeft,[status(thm)],[c_578]) ).
tff(c_868,plain,
c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_sko__uTE(v_x,v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb))) = v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb),
inference(resolution,[status(thm)],[c_847,c_16]) ).
tff(c_1209,plain,
! [V_y_113] : c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb),V_y_113),v_sko__uTE(v_x,v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb)),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)),
inference(superposition,[status(thm),theory(equality)],[c_868,c_22]) ).
tff(c_1218,plain,
c_in(c_Pair(v_xb,v_sko__uTE(v_x,v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb)),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)),
inference(superposition,[status(thm),theory(equality)],[c_580,c_1209]) ).
tff(c_1230,plain,
~ c_in(c_Pair(v_x,v_sko__uTE(v_x,v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb)),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)),
inference(resolution,[status(thm)],[c_1218,c_4]) ).
tff(c_1236,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_867,c_1230]) ).
tff(c_1237,plain,
( ( c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_xb) = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x) )
| ( c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTF(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb)),v_sko__uTG(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb)) = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x) ) ),
inference(splitRight,[status(thm)],[c_846]) ).
tff(c_1239,plain,
c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTF(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb)),v_sko__uTG(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb)) = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),
inference(splitLeft,[status(thm)],[c_1237]) ).
tff(c_12,plain,
! [V_comb1_H_12,V_comb1_10,V_comb2_H_13,V_comb2_11] :
( ( V_comb1_H_12 = V_comb1_10 )
| ( c_Comb_Ocomb_Oop_A_D_D(V_comb1_H_12,V_comb2_H_13) != c_Comb_Ocomb_Oop_A_D_D(V_comb1_10,V_comb2_11) ) ),
inference(cnfTransformation,[status(thm)],[f_62]) ).
tff(c_1285,plain,
! [V_comb1_H_12,V_comb2_H_13] :
( ( c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTF(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb)) = V_comb1_H_12 )
| ( c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x) != c_Comb_Ocomb_Oop_A_D_D(V_comb1_H_12,V_comb2_H_13) ) ),
inference(superposition,[status(thm),theory(equality)],[c_1239,c_12]) ).
tff(c_1432,plain,
c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTF(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb)) = c_Comb_Ocomb_OK,
inference(reflexivity,[status(thm),theory(equality)],[c_1285]) ).
tff(c_1434,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_10,c_1432]) ).
tff(c_1435,plain,
c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_xb) = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),
inference(splitRight,[status(thm)],[c_1237]) ).
tff(c_150,plain,
c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_sko__uTE(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya),c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_xb))) = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_xb),
inference(resolution,[status(thm)],[c_2,c_135]) ).
tff(c_292,plain,
! [V_comb2_H_70,V_y_71] : ( v_sko__uTE(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,V_comb2_H_70),V_y_71),c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,V_comb2_H_70)) = V_comb2_H_70 ),
inference(reflexivity,[status(thm),theory(equality)],[c_191]) ).
tff(c_301,plain,
! [V_y_71] : ( v_sko__uTE(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_xb),V_y_71),c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_sko__uTE(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya),c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_xb)))) = v_sko__uTE(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya),c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_xb)) ),
inference(superposition,[status(thm),theory(equality)],[c_150,c_292]) ).
tff(c_307,plain,
v_sko__uTE(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya),c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_xb)) = v_xb,
inference(demodulation,[status(thm),theory(equality)],[c_278,c_150,c_301]) ).
tff(c_1437,plain,
v_sko__uTE(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya),c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x)) = v_xb,
inference(demodulation,[status(thm),theory(equality)],[c_1435,c_307]) ).
tff(c_1438,plain,
v_xb = v_x,
inference(demodulation,[status(thm),theory(equality)],[c_278,c_1437]) ).
tff(c_90,plain,
! [V_U_48] :
( ~ c_in(c_Pair(v_x,V_U_48,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| ~ c_in(c_Pair(v_xb,V_U_48,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)) ),
inference(cnfTransformation,[status(thm)],[f_32]) ).
tff(c_95,plain,
~ c_in(c_Pair(v_x,v_xb,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)),
inference(resolution,[status(thm)],[c_20,c_90]) ).
tff(c_1534,plain,
~ c_in(c_Pair(v_x,v_x,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)),
inference(demodulation,[status(thm),theory(equality)],[c_1438,c_95]) ).
tff(c_1539,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_20,c_1534]) ).
tff(c_1540,plain,
( ( c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTF(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb)),v_sko__uTG(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb)) = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x) )
| ( c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_xb) = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x) ) ),
inference(splitRight,[status(thm)],[c_578]) ).
tff(c_1542,plain,
c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_xb) = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),
inference(splitLeft,[status(thm)],[c_1540]) ).
tff(c_1543,plain,
v_sko__uTE(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya),c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x)) = v_xb,
inference(demodulation,[status(thm),theory(equality)],[c_1542,c_307]) ).
tff(c_1544,plain,
v_xb = v_x,
inference(demodulation,[status(thm),theory(equality)],[c_278,c_1543]) ).
tff(c_1619,plain,
~ c_in(c_Pair(v_x,v_x,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)),
inference(demodulation,[status(thm),theory(equality)],[c_1544,c_95]) ).
tff(c_1624,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_20,c_1619]) ).
tff(c_1625,plain,
c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTF(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb)),v_sko__uTG(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb)) = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),
inference(splitRight,[status(thm)],[c_1540]) ).
tff(c_1655,plain,
! [V_comb1_H_12,V_comb2_H_13] :
( ( c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTF(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb)) = V_comb1_H_12 )
| ( c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x) != c_Comb_Ocomb_Oop_A_D_D(V_comb1_H_12,V_comb2_H_13) ) ),
inference(superposition,[status(thm),theory(equality)],[c_1625,c_12]) ).
tff(c_1732,plain,
c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTF(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb)) = c_Comb_Ocomb_OK,
inference(reflexivity,[status(thm),theory(equality)],[c_1655]) ).
tff(c_1734,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_10,c_1732]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.13/0.14 % Problem : COL106-2 : TPTP v9.0.0. Released v3.2.0.
% 0.13/0.15 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.15/0.36 % Computer : n031.cluster.edu
% 0.15/0.36 % Model : x86_64 x86_64
% 0.15/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.36 % Memory : 8042.1875MB
% 0.15/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.36 % CPULimit : 300
% 0.15/0.36 % WCLimit : 300
% 0.15/0.36 % DateTime : Mon Apr 7 16:06:07 EDT 2025
% 0.15/0.36 % CPUTime :
% 5.26/2.37 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 5.60/2.38
% 5.60/2.38 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------