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