Gary is big. Gary is nice. Gary is smart. All kind things are quiet. If something is red and cold then it is kind. If something is red then it is big. If Gary is red and Gary is big then Gary is kind. Smart things are red. Big, smart things are cold. All red things are nice. If something is big then it is nice.
Gary is big.
("Gary" "is" "big" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is smart.
("Gary" "is" "smart" "+")
All kind things are quiet.
((("something" "is" "kind" "+")) -> ("something" "is" "quiet" "+"))
If something is red and cold then it is kind.
((("something" "is" "red" "+") ("something" "is" "cold" "+")) -> ("something" "is" "kind" "+"))
If something is red then it is big.
((("something" "is" "red" "+")) -> ("something" "is" "big" "+"))
If Gary is red and Gary is big then Gary is kind.
((("Gary" "is" "red" "+") ("Gary" "is" "big" "+")) -> ("Gary" "is" "kind" "+"))
Smart things are red.
((("something" "is" "smart" "+")) -> ("something" "is" "red" "+"))
Big, smart things are cold.
((("something" "is" "big" "+") ("something" "is" "smart" "+")) -> ("something" "is" "cold" "+"))
All red things are nice.
((("something" "is" "red" "+")) -> ("something" "is" "nice" "+"))
If something is big then it is nice.
((("something" "is" "big" "+")) -> ("something" "is" "nice" "+"))
Gary is big.
True
1
proof
[(triple1 OR ((((triple3) -> rule5)) -> rule3))]
("Gary" "is" "big" "+")
triple1
((((triple3) -> (rule5 % int2))) -> (rule3 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is not nice.
False
1
inv-proof
[(triple2 OR ((triple1) -> rule8) OR ((((triple3) -> rule5)) -> rule7) OR ((((((triple3) -> rule5)) -> rule3)) -> rule8))]
("Gary" "is" "nice" "-")
triple2
((triple1) -> (rule8 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
((((triple3) -> (rule5 % int2))) -> (rule7 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
((((((triple3) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
Gary is red.
True
2
proof
[(((triple3) -> rule5))]
("Gary" "is" "red" "+")
((triple3) -> (rule5 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is not red.
False
2
inv-proof
[(((triple3) -> rule5))]
("Gary" "is" "red" "-")
((triple3) -> (rule5 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is kind.
True
4
proof
[(((((triple3) -> rule5) triple1) -> rule4) OR ((((triple3) -> rule5) ((triple1 triple3) -> rule6)) -> rule2) OR ((((triple3) -> rule5) ((((triple3) -> rule5)) -> rule3)) -> rule4) OR ((((triple3) -> rule5) ((((((triple3) -> rule5)) -> rule3) triple3) -> rule6)) -> rule2))]
("Gary" "is" "kind" "+")
((((triple3) -> (rule5 % int2)) triple1) -> (rule4 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
((((triple3) -> (rule5 % int3)) ((triple1 triple3) -> (rule6 % int2))) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
((((triple3) -> (rule5 % int3)) ((((triple3) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
((((triple3) -> (rule5 % int4)) ((((((triple3) -> (rule5 % int4))) -> (rule3 % int3)) triple3) -> (rule6 % int2))) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
Gary is red.
("Gary" "is" "red" "+")
int4
Gary is not kind.
False
4
inv-proof
[(((((triple3) -> rule5) triple1) -> rule4) OR ((((triple3) -> rule5) ((triple1 triple3) -> rule6)) -> rule2) OR ((((triple3) -> rule5) ((((triple3) -> rule5)) -> rule3)) -> rule4) OR ((((triple3) -> rule5) ((((((triple3) -> rule5)) -> rule3) triple3) -> rule6)) -> rule2))]
("Gary" "is" "kind" "-")
((((triple3) -> (rule5 % int2)) triple1) -> (rule4 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
((((triple3) -> (rule5 % int3)) ((triple1 triple3) -> (rule6 % int2))) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
((((triple3) -> (rule5 % int3)) ((((triple3) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
((((triple3) -> (rule5 % int4)) ((((((triple3) -> (rule5 % int4))) -> (rule3 % int3)) triple3) -> (rule6 % int2))) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
Gary is red.
("Gary" "is" "red" "+")
int4
Gary is quiet.
True
5
proof
[(((((((triple3) -> rule5) triple1) -> rule4)) -> rule1) OR ((((((triple3) -> rule5) ((triple1 triple3) -> rule6)) -> rule2)) -> rule1) OR ((((((triple3) -> rule5) ((((triple3) -> rule5)) -> rule3)) -> rule4)) -> rule1) OR ((((((triple3) -> rule5) ((((((triple3) -> rule5)) -> rule3) triple3) -> rule6)) -> rule2)) -> rule1))]
("Gary" "is" "quiet" "+")
((((((triple3) -> (rule5 % int3)) triple1) -> (rule4 % int2))) -> (rule1 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
((((((triple3) -> (rule5 % int4)) ((triple1 triple3) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Gary is red.
("Gary" "is" "red" "+")
int4
((((((triple3) -> (rule5 % int4)) ((((triple3) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
Gary is red.
("Gary" "is" "red" "+")
int4
((((((triple3) -> (rule5 % int5)) ((((((triple3) -> (rule5 % int5))) -> (rule3 % int4)) triple3) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Gary is big.
("Gary" "is" "big" "+")
int4
Gary is red.
("Gary" "is" "red" "+")
int5
Gary is not quiet.
False
5
inv-proof
[(((((((triple3) -> rule5) triple1) -> rule4)) -> rule1) OR ((((((triple3) -> rule5) ((triple1 triple3) -> rule6)) -> rule2)) -> rule1) OR ((((((triple3) -> rule5) ((((triple3) -> rule5)) -> rule3)) -> rule4)) -> rule1) OR ((((((triple3) -> rule5) ((((((triple3) -> rule5)) -> rule3) triple3) -> rule6)) -> rule2)) -> rule1))]
("Gary" "is" "quiet" "-")
((((((triple3) -> (rule5 % int3)) triple1) -> (rule4 % int2))) -> (rule1 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
((((((triple3) -> (rule5 % int4)) ((triple1 triple3) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Gary is red.
("Gary" "is" "red" "+")
int4
((((((triple3) -> (rule5 % int4)) ((((triple3) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
Gary is red.
("Gary" "is" "red" "+")
int4
((((((triple3) -> (rule5 % int5)) ((((((triple3) -> (rule5 % int5))) -> (rule3 % int4)) triple3) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Gary is big.
("Gary" "is" "big" "+")
int4
Gary is red.
("Gary" "is" "red" "+")
int5
@0: Gary is big.[(triple1 OR ((((triple3) -> rule5)) -> rule3))] Gary is nice.[(triple2 OR ((triple1) -> rule8) OR ((((triple3) -> rule5)) -> rule7) OR ((((((triple3) -> rule5)) -> rule3)) -> rule8))] Gary is smart.[(triple3)] @1: Gary is cold.[(((triple1 triple3) -> rule6) OR ((((((triple3) -> rule5)) -> rule3) triple3) -> rule6))] Gary is red.[(((triple3) -> rule5))] @2: Gary is kind.[(((((triple3) -> rule5) triple1) -> rule4) OR ((((triple3) -> rule5) ((triple1 triple3) -> rule6)) -> rule2) OR ((((triple3) -> rule5) ((((triple3) -> rule5)) -> rule3)) -> rule4) OR ((((triple3) -> rule5) ((((((triple3) -> rule5)) -> rule3) triple3) -> rule6)) -> rule2))] @3: Gary is quiet.[(((((((triple3) -> rule5) triple1) -> rule4)) -> rule1) OR ((((((triple3) -> rule5) ((triple1 triple3) -> rule6)) -> rule2)) -> rule1) OR ((((((triple3) -> rule5) ((((triple3) -> rule5)) -> rule3)) -> rule4)) -> rule1) OR ((((((triple3) -> rule5) ((((((triple3) -> rule5)) -> rule3) triple3) -> rule6)) -> rule2)) -> rule1))]
Gary is big.
("Gary" "is" "big" "+")
triple1
((((triple3) -> (rule5 % int2))) -> (rule3 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
triple2
((triple1) -> (rule8 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
((((triple3) -> (rule5 % int2))) -> (rule7 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
((((((triple3) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
Gary is smart.
("Gary" "is" "smart" "+")
triple3
Gary is cold.
("Gary" "is" "cold" "+")
((triple1 triple3) -> (rule6 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
((((((triple3) -> (rule5 % int3))) -> (rule3 % int2)) triple3) -> (rule6 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
Gary is red.
("Gary" "is" "red" "+")
((triple3) -> (rule5 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
((((triple3) -> (rule5 % int2)) triple1) -> (rule4 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
((((triple3) -> (rule5 % int3)) ((triple1 triple3) -> (rule6 % int2))) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
((((triple3) -> (rule5 % int3)) ((((triple3) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
((((triple3) -> (rule5 % int4)) ((((((triple3) -> (rule5 % int4))) -> (rule3 % int3)) triple3) -> (rule6 % int2))) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
Gary is red.
("Gary" "is" "red" "+")
int4
Gary is quiet.
("Gary" "is" "quiet" "+")
((((((triple3) -> (rule5 % int3)) triple1) -> (rule4 % int2))) -> (rule1 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
((((((triple3) -> (rule5 % int4)) ((triple1 triple3) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Gary is red.
("Gary" "is" "red" "+")
int4
((((((triple3) -> (rule5 % int4)) ((((triple3) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
Gary is red.
("Gary" "is" "red" "+")
int4
((((((triple3) -> (rule5 % int5)) ((((((triple3) -> (rule5 % int5))) -> (rule3 % int4)) triple3) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Gary is big.
("Gary" "is" "big" "+")
int4
Gary is red.
("Gary" "is" "red" "+")
int5