%------------------------------------------------------------------------------
% File : CiME---2.01
% Problem : SWV918-10 : TPTP v7.3.0. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : tptp2X_and_run_cime %s
% Computer : n186.star.cs.uiowa.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2609 0 2.40GHz
% Memory : 32218.5MB
% OS : Linux 3.10.0-862.11.6.el7.x86_64
% CPULimit : 300s
% DateTime : Wed Feb 27 14:51:43 EST 2019
% Result : Satisfiable 1.19s
% Output : Assurance 0s
% Verified :
% SZS Type : None (Parsing solution fails)
% Syntax : Number of formulae : 0
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SWV918-10 : TPTP v7.3.0. Released v7.3.0.
% 0.00/0.04 % Command : tptp2X_and_run_cime %s
% 0.03/0.27 % Computer : n186.star.cs.uiowa.edu
% 0.03/0.27 % Model : x86_64 x86_64
% 0.03/0.27 % CPU : Intel(R) Xeon(R) CPU E5-2609 0 @ 2.40GHz
% 0.03/0.27 % Memory : 32218.5MB
% 0.03/0.27 % OS : Linux 3.10.0-862.11.6.el7.x86_64
% 0.03/0.27 % CPULimit : 300
% 0.03/0.27 % DateTime : Mon Feb 25 14:15:59 CST 2019
% 0.03/0.27 % CPUTime :
% 1.14/1.46 Processing problem /tmp/CiME_7845_n186.star.cs.uiowa.edu
% 1.14/1.46 #verbose 1;
% 1.14/1.46 let F = signature " tc_nat,tc_Value_Oval,v_FDTs____,v_C____,v_a____,v_h_Ha____,t_a,tc_String_Ochar,v_ha____,v_P,true : constant; c_fequal : 3; c_Option_Ooption_ONone : 1; hAPP : 2; c_Conform_Ooconf : 4; c_Fun_Ofun__upd : 5; c_Option_Ooption_OSome : 2; c_Pair : 4; tc_fun : 2; tc_Option_Ooption : 1; c_Objects_Oinit__fields : 1; tc_prod : 2; tc_Expr_Oexp : 1; tc_List_Olist : 1; c_Exceptions_Opreallocated : 1; c_Conform_Ohconf : 3; c_COMBI : 2; ifeq : 4; ifeq2 : 4;";
% 1.14/1.46 let X = vars "A B C V_P T_a V_h V_x V_X V_Y";
% 1.14/1.46 let Axioms = equations F X "
% 1.14/1.46 ifeq2(A,A,B,C) = B;
% 1.14/1.46 ifeq(A,A,B,C) = B;
% 1.14/1.46 c_COMBI(V_P,T_a) = V_P;
% 1.14/1.46 ifeq(c_Conform_Ohconf(V_P,V_h,T_a),true,c_Exceptions_Opreallocated(V_h),true) = true;
% 1.14/1.46 c_Conform_Ohconf(v_P,v_ha____,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))) = true;
% 1.14/1.46 c_COMBI(v_P,t_a) = v_P;
% 1.14/1.46 v_h_Ha____ = c_Fun_Ofun__upd(v_ha____,v_a____,c_Option_Ooption_OSome(c_Pair(v_C____,c_Objects_Oinit__fields(v_FDTs____),tc_List_Olist(tc_String_Ochar),tc_fun(tc_prod(tc_List_Olist(tc_String_Ochar),tc_List_Olist(tc_String_Ochar)),tc_Option_Ooption(tc_Value_Oval))),tc_prod(tc_List_Olist(tc_String_Ochar),tc_fun(tc_prod(tc_List_Olist(tc_String_Ochar),tc_List_Olist(tc_String_Ochar)),tc_Option_Ooption(tc_Value_Oval)))),tc_nat,tc_Option_Ooption(tc_prod(tc_List_Olist(tc_String_Ochar),tc_fun(tc_prod(tc_List_Olist(tc_String_Ochar),tc_List_Olist(tc_String_Ochar)),tc_Option_Ooption(tc_Value_Oval)))));
% 1.14/1.46 c_Conform_Ooconf(v_P,v_ha____,c_Pair(v_C____,c_Objects_Oinit__fields(v_FDTs____),tc_List_Olist(tc_String_Ochar),tc_fun(tc_prod(tc_List_Olist(tc_String_Ochar),tc_List_Olist(tc_String_Ochar)),tc_Option_Ooption(tc_Value_Oval))),tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))) = true;
% 1.14/1.46 hAPP(v_ha____,v_a____) = c_Option_Ooption_ONone(tc_prod(tc_List_Olist(tc_String_Ochar),tc_fun(tc_prod(tc_List_Olist(tc_String_Ochar),tc_List_Olist(tc_String_Ochar)),tc_Option_Ooption(tc_Value_Oval))));
% 1.14/1.46 c_fequal(V_x,V_x,T_a) = true;
% 1.14/1.46 ifeq2(c_fequal(V_X,V_Y,T_a),true,V_X,V_Y) = V_Y;
% 1.14/1.46 ";
% 1.14/1.46
% 1.14/1.46 let s1 = status F "
% 1.14/1.46 c_fequal lr_lex;
% 1.14/1.46 c_Option_Ooption_ONone lr_lex;
% 1.14/1.46 hAPP lr_lex;
% 1.14/1.46 c_Conform_Ooconf lr_lex;
% 1.14/1.46 c_Fun_Ofun__upd lr_lex;
% 1.14/1.46 tc_nat lr_lex;
% 1.14/1.46 c_Option_Ooption_OSome lr_lex;
% 1.14/1.46 c_Pair lr_lex;
% 1.14/1.46 tc_fun lr_lex;
% 1.14/1.46 tc_Option_Ooption lr_lex;
% 1.14/1.46 tc_Value_Oval lr_lex;
% 1.14/1.46 c_Objects_Oinit__fields lr_lex;
% 1.14/1.46 v_FDTs____ lr_lex;
% 1.14/1.46 v_C____ lr_lex;
% 1.14/1.46 v_a____ lr_lex;
% 1.14/1.46 v_h_Ha____ lr_lex;
% 1.14/1.46 t_a lr_lex;
% 1.14/1.46 tc_prod lr_lex;
% 1.14/1.46 tc_Expr_Oexp lr_lex;
% 1.14/1.46 tc_List_Olist lr_lex;
% 1.14/1.46 tc_String_Ochar lr_lex;
% 1.14/1.46 v_ha____ lr_lex;
% 1.14/1.46 v_P lr_lex;
% 1.14/1.46 c_Exceptions_Opreallocated lr_lex;
% 1.14/1.46 true lr_lex;
% 1.14/1.46 c_Conform_Ohconf lr_lex;
% 1.14/1.46 c_COMBI lr_lex;
% 1.14/1.46 ifeq lr_lex;
% 1.14/1.46 ifeq2 lr_lex;
% 1.14/1.46 ";
% 1.14/1.46
% 1.14/1.46 let p1 = precedence F "
% 1.14/1.46 c_Option_Ooption_OSome > c_Exceptions_Opreallocated > c_Fun_Ofun__upd > ifeq2 > ifeq > c_Pair > c_Conform_Ooconf > c_Conform_Ohconf > c_fequal > c_COMBI > tc_prod > tc_fun > hAPP > tc_List_Olist > tc_Expr_Oexp > c_Objects_Oinit__fields > tc_Option_Ooption > c_Option_Ooption_ONone > true > v_P > v_ha____ > tc_String_Ochar > t_a > v_h_Ha____ > v_a____ > v_C____ > v_FDTs____ > tc_Value_Oval > tc_nat";
% 1.14/1.46
% 1.14/1.46 let s2 = status F "
% 1.14/1.46 c_fequal mul;
% 1.14/1.46 c_Option_Ooption_ONone mul;
% 1.14/1.46 hAPP mul;
% 1.14/1.46 c_Conform_Ooconf mul;
% 1.14/1.46 c_Fun_Ofun__upd mul;
% 1.14/1.46 tc_nat mul;
% 1.14/1.46 c_Option_Ooption_OSome mul;
% 1.14/1.46 c_Pair mul;
% 1.14/1.46 tc_fun mul;
% 1.14/1.46 tc_Option_Ooption mul;
% 1.14/1.46 tc_Value_Oval mul;
% 1.14/1.46 c_Objects_Oinit__fields mul;
% 1.14/1.46 v_FDTs____ mul;
% 1.14/1.46 v_C____ mul;
% 1.14/1.46 v_a____ mul;
% 1.14/1.46 v_h_Ha____ mul;
% 1.14/1.46 t_a mul;
% 1.14/1.46 tc_prod mul;
% 1.14/1.46 tc_Expr_Oexp mul;
% 1.14/1.46 tc_List_Olist mul;
% 1.14/1.46 tc_String_Ochar mul;
% 1.14/1.46 v_ha____ mul;
% 1.14/1.46 v_P mul;
% 1.14/1.46 c_Exceptions_Opreallocated mul;
% 1.14/1.46 true mul;
% 1.14/1.46 c_Conform_Ohconf mul;
% 1.14/1.46 c_COMBI mul;
% 1.14/1.46 ifeq mul;
% 1.14/1.46 ifeq2 mul;
% 1.14/1.46 ";
% 1.14/1.46
% 1.14/1.46 let p2 = precedence F "
% 1.14/1.46 c_Option_Ooption_OSome > c_Exceptions_Opreallocated > c_Fun_Ofun__upd > ifeq2 > ifeq > c_Pair > c_Conform_Ooconf > c_Conform_Ohconf > c_fequal > c_COMBI > tc_prod > tc_fun > hAPP > tc_List_Olist > tc_Expr_Oexp > c_Objects_Oinit__fields > tc_Option_Ooption > c_Option_Ooption_ONone > true = v_P = v_ha____ = tc_String_Ochar = t_a = v_h_Ha____ = v_a____ = v_C____ = v_FDTs____ = tc_Value_Oval = tc_nat";
% 1.14/1.47
% 1.14/1.47 let o_auto = AUTO Axioms;
% 1.14/1.47
% 1.14/1.47 let o = LEX o_auto (LEX (ACRPO s1 p1) (ACRPO s2 p2));
% 1.14/1.47
% 1.14/1.47 let Conjectures = equations F X " c_Conform_Ohconf(v_P,v_h_Ha____,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))) = true;"
% 1.14/1.47 ;
% 1.14/1.47 (*
% 1.14/1.47 let Red_Axioms = normalize_equations Defining_rules Axioms;
% 1.14/1.47
% 1.14/1.47 let Red_Conjectures = normalize_equations Defining_rules Conjectures;
% 1.14/1.47 *)
% 1.14/1.47 #time on;
% 1.14/1.47
% 1.14/1.47 let res = prove_conj_by_ordered_completion o Axioms Conjectures;
% 1.14/1.47
% 1.14/1.47 #time off;
% 1.14/1.47
% 1.14/1.47
% 1.14/1.47 let status = if res then "unsatisfiable" else "satisfiable";
% 1.14/1.47 #quit;
% 1.14/1.47 Verbose level is now 1
% 1.14/1.47
% 1.14/1.47 F : signature = <signature>
% 1.14/1.47 X : variable_set = <variable set>
% 1.14/1.47
% 1.14/1.47 Axioms : (F,X) equations = { ifeq2(A,A,B,C) = B,
% 1.14/1.47 ifeq(A,A,B,C) = B,
% 1.14/1.47 c_COMBI(V_P,T_a) = V_P,
% 1.14/1.47 ifeq(c_Conform_Ohconf(V_P,V_h,T_a),true,
% 1.14/1.47 c_Exceptions_Opreallocated(V_h),true) = true,
% 1.14/1.47 c_Conform_Ohconf(v_P,v_ha____,tc_prod(tc_List_Olist(
% 1.14/1.47 tc_List_Olist(tc_String_Ochar)),
% 1.14/1.47 tc_Expr_Oexp(
% 1.14/1.47 tc_List_Olist(tc_String_Ochar))))
% 1.14/1.47 = true,
% 1.14/1.47 c_COMBI(v_P,t_a) = v_P,
% 1.14/1.47 v_h_Ha____ =
% 1.14/1.47 c_Fun_Ofun__upd(v_ha____,v_a____,c_Option_Ooption_OSome(
% 1.14/1.47 c_Pair(v_C____,
% 1.14/1.47 c_Objects_Oinit__fields(v_FDTs____),
% 1.14/1.47 tc_List_Olist(tc_String_Ochar),
% 1.14/1.47 tc_fun(
% 1.14/1.47 tc_prod(
% 1.14/1.47 tc_List_Olist(tc_String_Ochar),
% 1.14/1.47 tc_List_Olist(tc_String_Ochar)),
% 1.14/1.47 tc_Option_Ooption(tc_Value_Oval))),
% 1.14/1.47 tc_prod(
% 1.14/1.47 tc_List_Olist(tc_String_Ochar),
% 1.14/1.47 tc_fun(
% 1.14/1.47 tc_prod(
% 1.14/1.47 tc_List_Olist(tc_String_Ochar),
% 1.14/1.47 tc_List_Olist(tc_String_Ochar)),
% 1.14/1.47 tc_Option_Ooption(tc_Value_Oval)))),tc_nat,
% 1.14/1.47 tc_Option_Ooption(tc_prod(tc_List_Olist(tc_String_Ochar),
% 1.14/1.47 tc_fun(tc_prod(tc_List_Olist(tc_String_Ochar),
% 1.14/1.47 tc_List_Olist(tc_String_Ochar)),
% 1.14/1.47 tc_Option_Ooption(tc_Value_Oval))))),
% 1.14/1.47 c_Conform_Ooconf(v_P,v_ha____,c_Pair(v_C____,
% 1.14/1.47 c_Objects_Oinit__fields(v_FDTs____),
% 1.14/1.47 tc_List_Olist(tc_String_Ochar),
% 1.14/1.47 tc_fun(tc_prod(
% 1.14/1.47 tc_List_Olist(tc_String_Ochar),
% 1.14/1.47 tc_List_Olist(tc_String_Ochar)),
% 1.14/1.47 tc_Option_Ooption(tc_Value_Oval))),
% 1.14/1.47 tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),
% 1.14/1.47 tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))) =
% 1.14/1.47 true,
% 1.14/1.47 hAPP(v_ha____,v_a____) =
% 1.19/1.48 c_Option_Ooption_ONone(tc_prod(tc_List_Olist(tc_String_Ochar),
% 1.19/1.48 tc_fun(tc_prod(tc_List_Olist(tc_String_Ochar),
% 1.19/1.48 tc_List_Olist(tc_String_Ochar)),
% 1.19/1.48 tc_Option_Ooption(tc_Value_Oval)))),
% 1.19/1.48 c_fequal(V_x,V_x,T_a) = true,
% 1.19/1.48 ifeq2(c_fequal(V_X,V_Y,T_a),true,V_X,V_Y) = V_Y }
% 1.19/1.48 (11 equation(s))
% 1.19/1.48 s1 : F status = <status>
% 1.19/1.48 p1 : F precedence = <precedence>
% 1.19/1.48 s2 : F status = <status>
% 1.19/1.48 p2 : F precedence = <precedence>
% 1.19/1.48 o_auto : F term_ordering = <term ordering>
% 1.19/1.48 o : F term_ordering = <term ordering>
% 1.19/1.48 Conjectures : (F,X) equations = { c_Conform_Ohconf(v_P,v_h_Ha____,tc_prod(
% 1.19/1.48 tc_List_Olist(
% 1.19/1.48 tc_List_Olist(tc_String_Ochar)),
% 1.19/1.48 tc_Expr_Oexp(
% 1.19/1.48 tc_List_Olist(tc_String_Ochar))))
% 1.19/1.48 = true } (1 equation(s))
% 1.19/1.48 time is now on
% 1.19/1.48
% 1.19/1.48 Initializing completion ...
% 1.19/1.48 New rule produced : [1] c_COMBI(V_P,T_a) -> V_P
% 1.19/1.48 Current number of equations to process: 0
% 1.19/1.48 Current number of ordered equations: 9
% 1.19/1.48 Current number of rules: 1
% 1.19/1.48 New rule produced : [2] c_fequal(V_x,V_x,T_a) -> true
% 1.19/1.48 Current number of equations to process: 0
% 1.19/1.48 Current number of ordered equations: 8
% 1.19/1.48 Current number of rules: 2
% 1.19/1.48 New rule produced : [3] ifeq(A,A,B,C) -> B
% 1.19/1.48 Current number of equations to process: 0
% 1.19/1.48 Current number of ordered equations: 7
% 1.19/1.48 Current number of rules: 3
% 1.19/1.48 New rule produced : [4] ifeq2(A,A,B,C) -> B
% 1.19/1.48 Current number of equations to process: 0
% 1.19/1.48 Current number of ordered equations: 6
% 1.19/1.48 Current number of rules: 4
% 1.19/1.48 New rule produced : [5] ifeq2(c_fequal(V_X,V_Y,T_a),true,V_X,V_Y) -> V_Y
% 1.19/1.48 Current number of equations to process: 0
% 1.19/1.48 Current number of ordered equations: 5
% 1.19/1.48 Current number of rules: 5
% 1.19/1.48 New rule produced :
% 1.19/1.48 [6]
% 1.19/1.48 ifeq(c_Conform_Ohconf(V_P,V_h,T_a),true,c_Exceptions_Opreallocated(V_h),true)
% 1.19/1.48 -> true
% 1.19/1.48 Current number of equations to process: 0
% 1.19/1.48 Current number of ordered equations: 4
% 1.19/1.48 Current number of rules: 6
% 1.19/1.48 New rule produced :
% 1.19/1.48 [7]
% 1.19/1.48 c_Conform_Ohconf(v_P,v_ha____,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),
% 1.19/1.48 tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar))))
% 1.19/1.48 -> true
% 1.19/1.48 Current number of equations to process: 0
% 1.19/1.48 Current number of ordered equations: 3
% 1.19/1.48 Current number of rules: 7
% 1.19/1.48 New rule produced :
% 1.19/1.48 [8]
% 1.19/1.48 c_Option_Ooption_ONone(tc_prod(tc_List_Olist(tc_String_Ochar),tc_fun(
% 1.19/1.48 tc_prod(
% 1.19/1.48 tc_List_Olist(tc_String_Ochar),
% 1.19/1.48 tc_List_Olist(tc_String_Ochar)),
% 1.19/1.48 tc_Option_Ooption(tc_Value_Oval))))
% 1.19/1.48 -> hAPP(v_ha____,v_a____)
% 1.19/1.48 Current number of equations to process: 0
% 1.19/1.48 Current number of ordered equations: 2
% 1.19/1.48 Current number of rules: 8
% 1.19/1.48 New rule produced :
% 1.19/1.48 [9]
% 1.19/1.48 c_Conform_Ooconf(v_P,v_ha____,c_Pair(v_C____,c_Objects_Oinit__fields(v_FDTs____),
% 1.19/1.48 tc_List_Olist(tc_String_Ochar),tc_fun(tc_prod(
% 1.19/1.48 tc_List_Olist(tc_String_Ochar),
% 1.19/1.48 tc_List_Olist(tc_String_Ochar)),
% 1.19/1.48 tc_Option_Ooption(tc_Value_Oval))),
% 1.19/1.48 tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar))))
% 1.19/1.48 -> true
% 1.19/1.48 Current number of equations to process: 0
% 1.19/1.48 Current number of ordered equations: 1
% 1.19/1.48 Current number of rules: 9
% 1.19/1.48 New rule produced :
% 1.19/1.48 [10]
% 1.19/1.48 c_Fun_Ofun__upd(v_ha____,v_a____,c_Option_Ooption_OSome(c_Pair(v_C____,
% 1.19/1.48 c_Objects_Oinit__fields(v_FDTs____),
% 1.19/1.48 tc_List_Olist(tc_String_Ochar),
% 1.19/1.48 tc_fun(tc_prod(
% 1.19/1.48 tc_List_Olist(tc_String_Ochar),
% 1.19/1.48 tc_List_Olist(tc_String_Ochar)),
% 1.19/1.48 tc_Option_Ooption(tc_Value_Oval))),
% 1.19/1.48 tc_prod(tc_List_Olist(tc_String_Ochar),
% 1.19/1.48 tc_fun(tc_prod(tc_List_Olist(tc_String_Ochar),
% 1.19/1.48 tc_List_Olist(tc_String_Ochar)),
% 1.19/1.48 tc_Option_Ooption(tc_Value_Oval)))),tc_nat,
% 1.19/1.48 tc_Option_Ooption(tc_prod(tc_List_Olist(tc_String_Ochar),tc_fun(tc_prod(
% 1.19/1.48 tc_List_Olist(tc_String_Ochar),
% 1.19/1.48 tc_List_Olist(tc_String_Ochar)),
% 1.19/1.48 tc_Option_Ooption(tc_Value_Oval)))))
% 1.19/1.48 -> v_h_Ha____
% 1.19/1.48 Current number of equations to process: 0
% 1.19/1.48 Current number of ordered equations: 0
% 1.19/1.48 Current number of rules: 10
% 1.19/1.48 New rule produced : [11] c_Exceptions_Opreallocated(v_ha____) -> true
% 1.19/1.48 Current number of equations to process: 0
% 1.19/1.48 Current number of ordered equations: 0
% 1.19/1.48 Current number of rules: 11
% 1.19/1.48 New rule produced :
% 1.19/1.48 [12] ifeq(c_Conform_Ohconf(A,v_ha____,B),true,true,true) -> true
% 1.19/1.48 Current number of equations to process: 0
% 1.19/1.48 Current number of ordered equations: 0
% 1.19/1.48 Current number of rules: 12
% 1.19/1.48 Warning: some conjectures remain
% 1.19/1.48
% 1.19/1.48 Execution time: 0.010000 sec
% 1.19/1.48 res : bool = false
% 1.19/1.48 time is now off
% 1.19/1.48
% 1.19/1.48 status : string = "satisfiable"
% 1.19/1.48 % SZS status Satisfiable
% 1.19/1.49 CiME interrupted
%------------------------------------------------------------------------------