Gary is blue. Gary is cold. Gary is kind. Gary is nice. Gary is quiet. Gary is red. Gary is white. If something is nice and blue then it is white. Kind things are white. If something is red and quiet then it is kind. All quiet things are red. If Gary is blue and Gary is cold then Gary is white. Red, white things are quiet.
Gary is blue.
("Gary" "is" "blue" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is white.
("Gary" "is" "white" "+")
If something is nice and blue then it is white.
((("something" "is" "nice" "+") ("something" "is" "blue" "+")) -> ("something" "is" "white" "+"))
Kind things are white.
((("something" "is" "kind" "+")) -> ("something" "is" "white" "+"))
If something is red and quiet then it is kind.
((("something" "is" "red" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "kind" "+"))
All quiet things are red.
((("something" "is" "quiet" "+")) -> ("something" "is" "red" "+"))
If Gary is blue and Gary is cold then Gary is white.
((("Gary" "is" "blue" "+") ("Gary" "is" "cold" "+")) -> ("Gary" "is" "white" "+"))
Red, white things are quiet.
((("something" "is" "red" "+") ("something" "is" "white" "+")) -> ("something" "is" "quiet" "+"))
Gary is blue.
True
1
proof
[(triple1)]
("Gary" "is" "blue" "+")
triple1
Gary is not red.
False
1
inv-proof
[(triple6 OR ((triple5) -> rule4))]
("Gary" "is" "red" "-")
triple6
((triple5) -> (rule4 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
@0: Gary is blue.[(triple1)] Gary is cold.[(triple2)] Gary is kind.[(triple3 OR ((triple6 triple5) -> rule3) OR ((triple6 ((triple6 triple7) -> rule6)) -> rule3) OR ((((triple5) -> rule4) triple5) -> rule3) OR ((((triple5) -> rule4) ((triple6 triple7) -> rule6)) -> rule3) OR ((triple6 ((triple6 ((triple1 triple2) -> rule5)) -> rule6)) -> rule3) OR ((triple6 ((triple6 ((triple4 triple1) -> rule1)) -> rule6)) -> rule3) OR ((((triple5) -> rule4) ((triple6 ((triple1 triple2) -> rule5)) -> rule6)) -> rule3) OR ((((triple5) -> rule4) ((triple6 ((triple4 triple1) -> rule1)) -> rule6)) -> rule3))] Gary is nice.[(triple4)] Gary is quiet.[(triple5 OR ((triple6 triple7) -> rule6) OR ((triple6 ((triple3) -> rule2)) -> rule6) OR ((triple6 ((triple1 triple2) -> rule5)) -> rule6) OR ((triple6 ((triple4 triple1) -> rule1)) -> rule6))] Gary is red.[(triple6 OR ((triple5) -> rule4))] Gary is white.[(triple7 OR ((triple3) -> rule2) OR ((triple1 triple2) -> rule5) OR ((triple4 triple1) -> rule1) OR ((((triple6 triple5) -> rule3)) -> rule2) OR ((((((triple5) -> rule4) triple5) -> rule3)) -> rule2))]
Gary is blue.
("Gary" "is" "blue" "+")
triple1
Gary is cold.
("Gary" "is" "cold" "+")
triple2
Gary is kind.
("Gary" "is" "kind" "+")
triple3
((triple6 triple5) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
((triple6 ((triple6 triple7) -> (rule6 % int2))) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
((((triple5) -> (rule4 % int2)) triple5) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
((((triple5) -> (rule4 % int3)) ((triple6 triple7) -> (rule6 % int2))) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
((triple6 ((triple6 ((triple1 triple2) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
((triple6 ((triple6 ((triple4 triple1) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
((((triple5) -> (rule4 % int4)) ((triple6 ((triple1 triple2) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Gary is red.
("Gary" "is" "red" "+")
int4
((((triple5) -> (rule4 % int4)) ((triple6 ((triple4 triple1) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Gary is red.
("Gary" "is" "red" "+")
int4
Gary is nice.
("Gary" "is" "nice" "+")
triple4
Gary is quiet.
("Gary" "is" "quiet" "+")
triple5
((triple6 triple7) -> (rule6 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
((triple6 ((triple3) -> (rule2 % int2))) -> (rule6 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
((triple6 ((triple1 triple2) -> (rule5 % int2))) -> (rule6 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
((triple6 ((triple4 triple1) -> (rule1 % int2))) -> (rule6 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
triple6
((triple5) -> (rule4 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
triple7
((triple3) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
((triple1 triple2) -> (rule5 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
((triple4 triple1) -> (rule1 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
((((triple6 triple5) -> (rule3 % int2))) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
((((((triple5) -> (rule4 % int3)) triple5) -> (rule3 % int2))) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3