Gary is blue. Gary is green. Gary is nice. Gary is quiet. Gary is red. Gary is rough. Gary is white. Green, quiet people are rough. All white people are rough. All quiet people are red. Red, rough people are white. Red people are blue. If Gary is red then Gary is nice.
Gary is blue.
("Gary" "is" "blue" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is white.
("Gary" "is" "white" "+")
Green, quiet people are rough.
((("someone" "is" "green" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "rough" "+"))
All white people are rough.
((("someone" "is" "white" "+")) -> ("someone" "is" "rough" "+"))
All quiet people are red.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "red" "+"))
Red, rough people are white.
((("someone" "is" "red" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "white" "+"))
Red people are blue.
((("someone" "is" "red" "+")) -> ("someone" "is" "blue" "+"))
If Gary is red then Gary is nice.
((("Gary" "is" "red" "+")) -> ("Gary" "is" "nice" "+"))
Gary is nice.
True
1
proof
[(triple3 OR ((triple5) -> rule6) OR ((((triple4) -> rule3)) -> rule6))]
("Gary" "is" "nice" "+")
triple3
((triple5) -> (rule6 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
((((triple4) -> (rule3 % int2))) -> (rule6 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is not white.
False
1
inv-proof
[(triple7 OR ((triple5 triple6) -> rule4) OR ((triple5 ((triple2 triple4) -> rule1)) -> rule4) OR ((((triple4) -> rule3) triple6) -> rule4) OR ((((triple4) -> rule3) ((triple2 triple4) -> rule1)) -> rule4))]
("Gary" "is" "white" "-")
triple7
((triple5 triple6) -> (rule4 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
((triple5 ((triple2 triple4) -> (rule1 % int2))) -> (rule4 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
((((triple4) -> (rule3 % int2)) triple6) -> (rule4 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
((((triple4) -> (rule3 % int3)) ((triple2 triple4) -> (rule1 % int2))) -> (rule4 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
@0: Gary is blue.[(triple1 OR ((triple5) -> rule5) OR ((((triple4) -> rule3)) -> rule5))] Gary is green.[(triple2)] Gary is nice.[(triple3 OR ((triple5) -> rule6) OR ((((triple4) -> rule3)) -> rule6))] Gary is quiet.[(triple4)] Gary is red.[(triple5 OR ((triple4) -> rule3))] Gary is rough.[(triple6 OR ((triple7) -> rule2) OR ((triple2 triple4) -> rule1))] Gary is white.[(triple7 OR ((triple5 triple6) -> rule4) OR ((triple5 ((triple2 triple4) -> rule1)) -> rule4) OR ((((triple4) -> rule3) triple6) -> rule4) OR ((((triple4) -> rule3) ((triple2 triple4) -> rule1)) -> rule4))]
Gary is blue.
("Gary" "is" "blue" "+")
triple1
((triple5) -> (rule5 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
((((triple4) -> (rule3 % int2))) -> (rule5 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
triple2
Gary is nice.
("Gary" "is" "nice" "+")
triple3
((triple5) -> (rule6 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
((((triple4) -> (rule3 % int2))) -> (rule6 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
triple4
Gary is red.
("Gary" "is" "red" "+")
triple5
((triple4) -> (rule3 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
triple6
((triple7) -> (rule2 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
((triple2 triple4) -> (rule1 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
triple7
((triple5 triple6) -> (rule4 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
((triple5 ((triple2 triple4) -> (rule1 % int2))) -> (rule4 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
((((triple4) -> (rule3 % int2)) triple6) -> (rule4 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
((((triple4) -> (rule3 % int3)) ((triple2 triple4) -> (rule1 % int2))) -> (rule4 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3