%---------------- SGGS v1.0 (IJCAR 2020 submission) ----------------% ------ Parsing...successful ------ Proving... use I- Gamma_0: (extend-no-conflict) 0: [c_lessequals(v_S,c_Tarski_Ointerval(v_r,v_a,v_b,t_a), tc_set(t_a))] Gamma_1: (extend-no-conflict) 0: [c_lessequals(v_S,c_Tarski_Ointerval(v_r,v_a,v_b,t_a), tc_set(t_a))] 1: [c_in(v_b,v_A,t_a)] Gamma_2: (extend-no-conflict) 0: [c_lessequals(v_S,c_Tarski_Ointerval(v_r,v_a,v_b,t_a), tc_set(t_a))] 1: [c_in(v_b,v_A,t_a)] 2: [c_in(v_a,v_A,t_a)] Gamma_3: (extend-no-conflict) 0: [c_lessequals(v_S,c_Tarski_Ointerval(v_r,v_a,v_b,t_a), tc_set(t_a))] 1: [c_in(v_b,v_A,t_a)] 2: [c_in(v_a,v_A,t_a)] 3: ~(c_lessequals(v_S,c_Tarski_Ointerval(v_r,v_a,v_b,t_a),tc_set(t_a))), [c_lessequals( v_S,v_A,tc_set(t_a))], ~(c_in(v_b,v_A,t_a)), ~(c_in(v_a,v_A,t_a)) Gamma_4: (extend-conflict) 0: [c_lessequals(v_S,c_Tarski_Ointerval(v_r,v_a,v_b,t_a), tc_set(t_a))] 1: [c_in(v_b,v_A,t_a)] 2: [c_in(v_a,v_A,t_a)] 3: ~(c_lessequals(v_S,c_Tarski_Ointerval(v_r,v_a,v_b,t_a),tc_set(t_a))), [c_lessequals( v_S,v_A,tc_set(t_a))], ~(c_in(v_b,v_A,t_a)), ~(c_in(v_a,v_A,t_a)) 4: [~(c_lessequals(v_S,v_A,tc_set(t_a)))] Gamma_5: (move) 0: [c_lessequals(v_S,c_Tarski_Ointerval(v_r,v_a,v_b,t_a), tc_set(t_a))] 1: [c_in(v_b,v_A,t_a)] 2: [c_in(v_a,v_A,t_a)] 3: [~(c_lessequals(v_S,v_A,tc_set(t_a)))] 4: ~(c_lessequals(v_S,c_Tarski_Ointerval(v_r,v_a,v_b,t_a),tc_set(t_a))), [c_lessequals( v_S,v_A,tc_set(t_a))], ~(c_in(v_b,v_A,t_a)), ~(c_in(v_a,v_A,t_a)) Gamma_6: (resolve) 0: [c_lessequals(v_S,c_Tarski_Ointerval(v_r,v_a,v_b,t_a), tc_set(t_a))] 1: [c_in(v_b,v_A,t_a)] 2: [c_in(v_a,v_A,t_a)] 3: [~(c_lessequals(v_S,v_A,tc_set(t_a)))] 4: [~(c_lessequals(v_S,c_Tarski_Ointerval(v_r,v_a,v_b,t_a),tc_set(t_a)))], ~( c_in(v_b,v_A,t_a)), ~(c_in(v_a,v_A,t_a)) Gamma_7: (extend-conflict) 0: [c_lessequals(v_S,c_Tarski_Ointerval(v_r,v_a,v_b,t_a), tc_set(t_a))] 1: [c_in(v_b,v_A,t_a)] 2: [c_in(v_a,v_A,t_a)] 3: [~(c_lessequals(v_S,v_A,tc_set(t_a)))] 4: ~(c_lessequals(v_S,c_Tarski_Ointerval(v_r,v_a,v_b,t_a),tc_set(t_a))), ~( c_in(v_b,v_A,t_a)), [~(c_in(v_a,v_A,t_a))] Gamma_8: (move) 0: [c_lessequals(v_S,c_Tarski_Ointerval(v_r,v_a,v_b,t_a), tc_set(t_a))] 1: [c_in(v_b,v_A,t_a)] 2: ~(c_lessequals(v_S,c_Tarski_Ointerval(v_r,v_a,v_b,t_a),tc_set(t_a))), ~( c_in(v_b,v_A,t_a)), [~(c_in(v_a,v_A,t_a))] 3: [c_in(v_a,v_A,t_a)] 4: [~(c_lessequals(v_S,v_A,tc_set(t_a)))] Gamma_9: (resolve) 0: [c_lessequals(v_S,c_Tarski_Ointerval(v_r,v_a,v_b,t_a), tc_set(t_a))] 1: [c_in(v_b,v_A,t_a)] 2: ~(c_lessequals(v_S,c_Tarski_Ointerval(v_r,v_a,v_b,t_a),tc_set(t_a))), ~( c_in(v_b,v_A,t_a)), [~(c_in(v_a,v_A,t_a))] 3: [~(c_lessequals(v_S,c_Tarski_Ointerval(v_r,v_a,v_b,t_a),tc_set(t_a)))], ~( c_in(v_b,v_A,t_a)) 4: [~(c_lessequals(v_S,v_A,tc_set(t_a)))] Gamma_10: (extend-conflict) 0: [c_lessequals(v_S,c_Tarski_Ointerval(v_r,v_a,v_b,t_a), tc_set(t_a))] 1: [c_in(v_b,v_A,t_a)] 2: ~(c_lessequals(v_S,c_Tarski_Ointerval(v_r,v_a,v_b,t_a),tc_set(t_a))), ~( c_in(v_b,v_A,t_a)), [~(c_in(v_a,v_A,t_a))] 3: ~(c_lessequals(v_S,c_Tarski_Ointerval(v_r,v_a,v_b,t_a),tc_set(t_a))), [~( c_in(v_b,v_A,t_a))] 4: [~(c_lessequals(v_S,v_A,tc_set(t_a)))] Gamma_11: (move) 0: [c_lessequals(v_S,c_Tarski_Ointerval(v_r,v_a,v_b,t_a), tc_set(t_a))] 1: ~(c_lessequals(v_S,c_Tarski_Ointerval(v_r,v_a,v_b,t_a),tc_set(t_a))), [~( c_in(v_b,v_A,t_a))] 2: [c_in(v_b,v_A,t_a)] 3: ~(c_lessequals(v_S,c_Tarski_Ointerval(v_r,v_a,v_b,t_a),tc_set(t_a))), ~( c_in(v_b,v_A,t_a)), [~(c_in(v_a,v_A,t_a))] 4: [~(c_lessequals(v_S,v_A,tc_set(t_a)))] Gamma_12: (resolve) 0: [c_lessequals(v_S,c_Tarski_Ointerval(v_r,v_a,v_b,t_a), tc_set(t_a))] 1: ~(c_lessequals(v_S,c_Tarski_Ointerval(v_r,v_a,v_b,t_a),tc_set(t_a))), [~( c_in(v_b,v_A,t_a))] 2: [~(c_lessequals(v_S,c_Tarski_Ointerval(v_r,v_a,v_b,t_a),tc_set(t_a)))] 3: [~(c_lessequals(v_S,v_A,tc_set(t_a)))] Gamma_13: (extend-conflict) 0: [c_lessequals(v_S,c_Tarski_Ointerval(v_r,v_a,v_b,t_a), tc_set(t_a))] 1: ~(c_lessequals(v_S,c_Tarski_Ointerval(v_r,v_a,v_b,t_a),tc_set(t_a))), [~( c_in(v_b,v_A,t_a))] 2: [~(c_lessequals(v_S,c_Tarski_Ointerval(v_r,v_a,v_b,t_a),tc_set(t_a)))] 3: [~(c_lessequals(v_S,v_A,tc_set(t_a)))] Gamma_14: (move) 0: [~(c_lessequals(v_S,c_Tarski_Ointerval(v_r,v_a,v_b,t_a),tc_set(t_a)))] 1: [c_lessequals(v_S,c_Tarski_Ointerval(v_r,v_a,v_b,t_a),tc_set(t_a))] 2: ~(c_lessequals(v_S,c_Tarski_Ointerval(v_r,v_a,v_b,t_a),tc_set(t_a))), [~( c_in(v_b,v_A,t_a))] 3: [~(c_lessequals(v_S,v_A,tc_set(t_a)))] Gamma_15: (resolve) 0: [~(c_lessequals(v_S,c_Tarski_Ointerval(v_r,v_a,v_b,t_a),tc_set(t_a)))] 1: [] 2: [~(c_lessequals(v_S,v_A,tc_set(t_a)))] SZS status Unsatisfiable %---------------- SGGS v1.0 (IJCAR 2020 submission) ----------------% ------ Parsing...successful ------ Proving... use I- Gamma_0: (extend-no-conflict) 0: [c_lessequals(v_S,c_Tarski_Ointerval(v_r,v_a,v_b,t_a), tc_set(t_a))] Gamma_1: (extend-no-conflict) 0: [c_lessequals(v_S,c_Tarski_Ointerval(v_r,v_a,v_b,t_a), tc_set(t_a))] 1: [c_in(v_b,v_A,t_a)] Gamma_2: (extend-no-conflict) 0: [c_lessequals(v_S,c_Tarski_Ointerval(v_r,v_a,v_b,t_a), tc_set(t_a))] 1: [c_in(v_b,v_A,t_a)] 2: [c_in(v_a,v_A,t_a)] Gamma_3: (extend-no-conflict) 0: [c_lessequals(v_S,c_Tarski_Ointerval(v_r,v_a,v_b,t_a), tc_set(t_a))] 1: [c_in(v_b,v_A,t_a)] 2: [c_in(v_a,v_A,t_a)] 3: ~(c_lessequals(v_S,c_Tarski_Ointerval(v_r,v_a,v_b,t_a),tc_set(t_a))), [c_lessequals( v_S,v_A,tc_set(t_a))], ~(c_in(v_b,v_A,t_a)), ~(c_in(v_a,v_A,t_a)) Gamma_4: (extend-conflict) 0: [c_lessequals(v_S,c_Tarski_Ointerval(v_r,v_a,v_b,t_a), tc_set(t_a))] 1: [c_in(v_b,v_A,t_a)] 2: [c_in(v_a,v_A,t_a)] 3: ~(c_lessequals(v_S,c_Tarski_Ointerval(v_r,v_a,v_b,t_a),tc_set(t_a))), [c_lessequals( v_S,v_A,tc_set(t_a))], ~(c_in(v_b,v_A,t_a)), ~(c_in(v_a,v_A,t_a)) 4: [~(c_lessequals(v_S,v_A,tc_set(t_a)))] Gamma_5: (move) 0: [c_lessequals(v_S,c_Tarski_Ointerval(v_r,v_a,v_b,t_a), tc_set(t_a))] 1: [c_in(v_b,v_A,t_a)] 2: [c_in(v_a,v_A,t_a)] 3: [~(c_lessequals(v_S,v_A,tc_set(t_a)))] 4: ~(c_lessequals(v_S,c_Tarski_Ointerval(v_r,v_a,v_b,t_a),tc_set(t_a))), [c_lessequals( v_S,v_A,tc_set(t_a))], ~(c_in(v_b,v_A,t_a)), ~(c_in(v_a,v_A,t_a)) Gamma_6: (resolve) 0: [c_lessequals(v_S,c_Tarski_Ointerval(v_r,v_a,v_b,t_a), tc_set(t_a))] 1: [c_in(v_b,v_A,t_a)] 2: [c_in(v_a,v_A,t_a)] 3: [~(c_lessequals(v_S,v_A,tc_set(t_a)))] 4: [~(c_lessequals(v_S,c_Tarski_Ointerval(v_r,v_a,v_b,t_a),tc_set(t_a)))], ~( c_in(v_b,v_A,t_a)), ~(c_in(v_a,v_A,t_a)) Gamma_7: (extend-conflict) 0: [c_lessequals(v_S,c_Tarski_Ointerval(v_r,v_a,v_b,t_a), tc_set(t_a))] 1: [c_in(v_b,v_A,t_a)] 2: [c_in(v_a,v_A,t_a)] 3: [~(c_lessequals(v_S,v_A,tc_set(t_a)))] 4: ~(c_lessequals(v_S,c_Tarski_Ointerval(v_r,v_a,v_b,t_a),tc_set(t_a))), ~( c_in(v_b,v_A,t_a)), [~(c_in(v_a,v_A,t_a))] Gamma_8: (move) 0: [c_lessequals(v_S,c_Tarski_Ointerval(v_r,v_a,v_b,t_a), tc_set(t_a))] 1: [c_in(v_b,v_A,t_a)] 2: ~(c_lessequals(v_S,c_Tarski_Ointerval(v_r,v_a,v_b,t_a),tc_set(t_a))), ~( c_in(v_b,v_A,t_a)), [~(c_in(v_a,v_A,t_a))] 3: [c_in(v_a,v_A,t_a)] 4: [~(c_lessequals(v_S,v_A,tc_set(t_a)))] Gamma_9: (resolve) 0: [c_lessequals(v_S,c_Tarski_Ointerval(v_r,v_a,v_b,t_a), tc_set(t_a))] 1: [c_in(v_b,v_A,t_a)] 2: ~(c_lessequals(v_S,c_Tarski_Ointerval(v_r,v_a,v_b,t_a),tc_set(t_a))), ~( c_in(v_b,v_A,t_a)), [~(c_in(v_a,v_A,t_a))] 3: [~(c_lessequals(v_S,c_Tarski_Ointerval(v_r,v_a,v_b,t_a),tc_set(t_a)))], ~( c_in(v_b,v_A,t_a)) 4: [~(c_lessequals(v_S,v_A,tc_set(t_a)))] Gamma_10: (extend-conflict) 0: [c_lessequals(v_S,c_Tarski_Ointerval(v_r,v_a,v_b,t_a), tc_set(t_a))] 1: [c_in(v_b,v_A,t_a)] 2: ~(c_lessequals(v_S,c_Tarski_Ointerval(v_r,v_a,v_b,t_a),tc_set(t_a))), ~( c_in(v_b,v_A,t_a)), [~(c_in(v_a,v_A,t_a))] 3: ~(c_lessequals(v_S,c_Tarski_Ointerval(v_r,v_a,v_b,t_a),tc_set(t_a))), [~( c_in(v_b,v_A,t_a))] 4: [~(c_lessequals(v_S,v_A,tc_set(t_a)))] Gamma_11: (move) 0: [c_lessequals(v_S,c_Tarski_Ointerval(v_r,v_a,v_b,t_a), tc_set(t_a))] 1: ~(c_lessequals(v_S,c_Tarski_Ointerval(v_r,v_a,v_b,t_a),tc_set(t_a))), [~( c_in(v_b,v_A,t_a))] 2: [c_in(v_b,v_A,t_a)] 3: ~(c_lessequals(v_S,c_Tarski_Ointerval(v_r,v_a,v_b,t_a),tc_set(t_a))), ~( c_in(v_b,v_A,t_a)), [~(c_in(v_a,v_A,t_a))] 4: [~(c_lessequals(v_S,v_A,tc_set(t_a)))] Gamma_12: (resolve) 0: [c_lessequals(v_S,c_Tarski_Ointerval(v_r,v_a,v_b,t_a), tc_set(t_a))] 1: ~(c_lessequals(v_S,c_Tarski_Ointerval(v_r,v_a,v_b,t_a),tc_set(t_a))), [~( c_in(v_b,v_A,t_a))] 2: [~(c_lessequals(v_S,c_Tarski_Ointerval(v_r,v_a,v_b,t_a),tc_set(t_a)))] 3: [~(c_lessequals(v_S,v_A,tc_set(t_a)))] Gamma_13: (extend-conflict) 0: [c_lessequals(v_S,c_Tarski_Ointerval(v_r,v_a,v_b,t_a), tc_set(t_a))] 1: ~(c_lessequals(v_S,c_Tarski_Ointerval(v_r,v_a,v_b,t_a),tc_set(t_a))), [~( c_in(v_b,v_A,t_a))] 2: [~(c_lessequals(v_S,c_Tarski_Ointerval(v_r,v_a,v_b,t_a),tc_set(t_a)))] 3: [~(c_lessequals(v_S,v_A,tc_set(t_a)))] Gamma_14: (move) 0: [~(c_lessequals(v_S,c_Tarski_Ointerval(v_r,v_a,v_b,t_a),tc_set(t_a)))] 1: [c_lessequals(v_S,c_Tarski_Ointerval(v_r,v_a,v_b,t_a),tc_set(t_a))] 2: ~(c_lessequals(v_S,c_Tarski_Ointerval(v_r,v_a,v_b,t_a),tc_set(t_a))), [~( c_in(v_b,v_A,t_a))] 3: [~(c_lessequals(v_S,v_A,tc_set(t_a)))] Gamma_15: (resolve) 0: [~(c_lessequals(v_S,c_Tarski_Ointerval(v_r,v_a,v_b,t_a),tc_set(t_a)))] 1: [] 2: [~(c_lessequals(v_S,v_A,tc_set(t_a)))] SZS status Unsatisfiable