Bob is not furry. Bob is kind. Bob is rough. Bob is round. Gary is big. Gary is furry. Gary is kind. Gary is red. Gary is not rough. Gary is round. All red, big things are round. If something is red then it is round. If something is red and big then it is kind. If something is quiet then it is red. All big things are quiet. All round things are big. If Gary is big and Gary is not rough then Gary is furry. If Gary is quiet and Gary is not red then Gary is not kind.
Bob is not furry.
("Bob" "is" "furry" "-")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is round.
("Bob" "is" "round" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is not rough.
("Gary" "is" "rough" "-")
Gary is round.
("Gary" "is" "round" "+")
All red, big things are round.
((("something" "is" "red" "+") ("something" "is" "big" "+")) -> ("something" "is" "round" "+"))
If something is red then it is round.
((("something" "is" "red" "+")) -> ("something" "is" "round" "+"))
If something is red and big then it is kind.
((("something" "is" "red" "+") ("something" "is" "big" "+")) -> ("something" "is" "kind" "+"))
If something is quiet then it is red.
((("something" "is" "quiet" "+")) -> ("something" "is" "red" "+"))
All big things are quiet.
((("something" "is" "big" "+")) -> ("something" "is" "quiet" "+"))
All round things are big.
((("something" "is" "round" "+")) -> ("something" "is" "big" "+"))
If Gary is big and Gary is not rough then Gary is furry.
((("Gary" "is" "big" "+") ("Gary" "is" "rough" "~")) -> ("Gary" "is" "furry" "+"))
If Gary is quiet and Gary is not red then Gary is not kind.
((("Gary" "is" "quiet" "+") ("Gary" "is" "red" "~")) -> ("Gary" "is" "kind" "-"))
Gary is kind.
True
1
proof
[(triple7 OR ((triple8 triple5) -> rule3) OR ((triple8 ((triple10) -> rule6)) -> rule3) OR ((triple8 ((((triple8) -> rule2)) -> rule6)) -> rule3) OR ((((((triple5) -> rule5)) -> rule4) triple5) -> rule3) OR ((((((triple5) -> rule5)) -> rule4) ((triple10) -> rule6)) -> rule3) OR ((((((triple5) -> rule5)) -> rule4) ((((triple8) -> rule2)) -> rule6)) -> rule3) OR ((((((((triple10) -> rule6)) -> rule5)) -> rule4) triple5) -> rule3) OR ((((((((triple10) -> rule6)) -> rule5)) -> rule4) ((triple10) -> rule6)) -> rule3) OR ((((((((triple10) -> rule6)) -> rule5)) -> rule4) ((((triple8) -> rule2)) -> rule6)) -> rule3))]
("Gary" "is" "kind" "+")
triple7
((triple8 triple5) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
((triple8 ((triple10) -> (rule6 % int2))) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
((triple8 ((((triple8) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
((((((triple5) -> (rule5 % int3))) -> (rule4 % int2)) triple5) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
((((((triple5) -> (rule5 % int4))) -> (rule4 % int3)) ((triple10) -> (rule6 % int2))) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
Gary is quiet.
("Gary" "is" "quiet" "+")
int4
((((((triple5) -> (rule5 % int5))) -> (rule4 % int4)) ((((triple8) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Gary is red.
("Gary" "is" "red" "+")
int4
Gary is quiet.
("Gary" "is" "quiet" "+")
int5
((((((((triple10) -> (rule6 % int4))) -> (rule5 % int3))) -> (rule4 % int2)) triple5) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Gary is big.
("Gary" "is" "big" "+")
int4
((((((((triple10) -> (rule6 % int4))) -> (rule5 % int3))) -> (rule4 % int2)) ((triple10) -> (rule6 % int4))) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Gary is big.
("Gary" "is" "big" "+")
int4
((((((((triple10) -> (rule6 % int5))) -> (rule5 % int4))) -> (rule4 % int3)) ((((triple8) -> (rule2 % int2))) -> (rule6 % int5))) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
Gary is quiet.
("Gary" "is" "quiet" "+")
int4
Gary is big.
("Gary" "is" "big" "+")
int5
Gary is not kind.
False
1
inv-proof
[(triple7 OR ((triple8 triple5) -> rule3) OR ((triple8 ((triple10) -> rule6)) -> rule3) OR ((triple8 ((((triple8) -> rule2)) -> rule6)) -> rule3) OR ((((((triple5) -> rule5)) -> rule4) triple5) -> rule3) OR ((((((triple5) -> rule5)) -> rule4) ((triple10) -> rule6)) -> rule3) OR ((((((triple5) -> rule5)) -> rule4) ((((triple8) -> rule2)) -> rule6)) -> rule3) OR ((((((((triple10) -> rule6)) -> rule5)) -> rule4) triple5) -> rule3) OR ((((((((triple10) -> rule6)) -> rule5)) -> rule4) ((triple10) -> rule6)) -> rule3) OR ((((((((triple10) -> rule6)) -> rule5)) -> rule4) ((((triple8) -> rule2)) -> rule6)) -> rule3))]
("Gary" "is" "kind" "-")
triple7
((triple8 triple5) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
((triple8 ((triple10) -> (rule6 % int2))) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
((triple8 ((((triple8) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
((((((triple5) -> (rule5 % int3))) -> (rule4 % int2)) triple5) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
((((((triple5) -> (rule5 % int4))) -> (rule4 % int3)) ((triple10) -> (rule6 % int2))) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
Gary is quiet.
("Gary" "is" "quiet" "+")
int4
((((((triple5) -> (rule5 % int5))) -> (rule4 % int4)) ((((triple8) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Gary is red.
("Gary" "is" "red" "+")
int4
Gary is quiet.
("Gary" "is" "quiet" "+")
int5
((((((((triple10) -> (rule6 % int4))) -> (rule5 % int3))) -> (rule4 % int2)) triple5) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Gary is big.
("Gary" "is" "big" "+")
int4
((((((((triple10) -> (rule6 % int4))) -> (rule5 % int3))) -> (rule4 % int2)) ((triple10) -> (rule6 % int4))) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Gary is big.
("Gary" "is" "big" "+")
int4
((((((((triple10) -> (rule6 % int5))) -> (rule5 % int4))) -> (rule4 % int3)) ((((triple8) -> (rule2 % int2))) -> (rule6 % int5))) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
Gary is quiet.
("Gary" "is" "quiet" "+")
int4
Gary is big.
("Gary" "is" "big" "+")
int5
Gary is quiet.
True
2
proof
[(((triple5) -> rule5) OR ((((triple10) -> rule6)) -> rule5) OR ((((((triple8) -> rule2)) -> rule6)) -> rule5))]
("Gary" "is" "quiet" "+")
((triple5) -> (rule5 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
((((triple10) -> (rule6 % int2))) -> (rule5 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
((((((triple8) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Bob is not big.
False
2
inv-proof
[(((triple4) -> rule6))]
("Bob" "is" "big" "-")
((triple4) -> (rule6 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is quiet.
True
3
proof
[(((((triple4) -> rule6)) -> rule5))]
("Bob" "is" "quiet" "+")
((((triple4) -> (rule6 % int2))) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is not quiet.
False
3
inv-proof
[(((((triple4) -> rule6)) -> rule5))]
("Bob" "is" "quiet" "-")
((((triple4) -> (rule6 % int2))) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is red.
True
4
proof
[(((((((triple4) -> rule6)) -> rule5)) -> rule4))]
("Bob" "is" "red" "+")
((((((triple4) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Bob is not red.
False
4
inv-proof
[(((((((triple4) -> rule6)) -> rule5)) -> rule4))]
("Bob" "is" "red" "-")
((((((triple4) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
@0: Bob is kind.[(triple2 OR ((((((((triple4) -> rule6)) -> rule5)) -> rule4) ((triple4) -> rule6)) -> rule3))] Bob is not furry.[(triple1)] Bob is rough.[(triple3)] Bob is round.[(triple4)] Gary is big.[(triple5 OR ((triple10) -> rule6) OR ((((triple8) -> rule2)) -> rule6))] Gary is furry.[(triple6 OR ((triple5 triple9) -> rule7) OR ((((triple10) -> rule6) triple9) -> rule7) OR ((((((triple8) -> rule2)) -> rule6) triple9) -> rule7))] Gary is kind.[(triple7 OR ((triple8 triple5) -> rule3) OR ((triple8 ((triple10) -> rule6)) -> rule3) OR ((triple8 ((((triple8) -> rule2)) -> rule6)) -> rule3) OR ((((((triple5) -> rule5)) -> rule4) triple5) -> rule3) OR ((((((triple5) -> rule5)) -> rule4) ((triple10) -> rule6)) -> rule3) OR ((((((triple5) -> rule5)) -> rule4) ((((triple8) -> rule2)) -> rule6)) -> rule3) OR ((((((((triple10) -> rule6)) -> rule5)) -> rule4) triple5) -> rule3) OR ((((((((triple10) -> rule6)) -> rule5)) -> rule4) ((triple10) -> rule6)) -> rule3) OR ((((((((triple10) -> rule6)) -> rule5)) -> rule4) ((((triple8) -> rule2)) -> rule6)) -> rule3))] Gary is not rough.[(triple9)] Gary is red.[(triple8 OR ((((triple5) -> rule5)) -> rule4) OR ((((((triple10) -> rule6)) -> rule5)) -> rule4))] Gary is round.[(triple10 OR ((triple8) -> rule2) OR ((triple8 triple5) -> rule1) OR ((((((triple5) -> rule5)) -> rule4)) -> rule2) OR ((((((triple5) -> rule5)) -> rule4) triple5) -> rule1))] @1: Bob is big.[(((triple4) -> rule6))] Gary is quiet.[(((triple5) -> rule5) OR ((((triple10) -> rule6)) -> rule5) OR ((((((triple8) -> rule2)) -> rule6)) -> rule5))] @2: Bob is quiet.[(((((triple4) -> rule6)) -> rule5))] @3: Bob is red.[(((((((triple4) -> rule6)) -> rule5)) -> rule4))]
Bob is kind.
("Bob" "is" "kind" "+")
triple2
((((((((triple4) -> (rule6 % int4))) -> (rule5 % int3))) -> (rule4 % int2)) ((triple4) -> (rule6 % int4))) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Bob is big.
("Bob" "is" "big" "+")
int4
Bob is not furry.
("Bob" "is" "furry" "-")
triple1
Bob is rough.
("Bob" "is" "rough" "+")
triple3
Bob is round.
("Bob" "is" "round" "+")
triple4
Gary is big.
("Gary" "is" "big" "+")
triple5
((triple10) -> (rule6 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
((((triple8) -> (rule2 % int2))) -> (rule6 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
triple6
((triple5 triple9) -> (rule7 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
((((triple10) -> (rule6 % int2)) triple9) -> (rule7 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
((((((triple8) -> (rule2 % int3))) -> (rule6 % int2)) triple9) -> (rule7 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Gary is kind.
("Gary" "is" "kind" "+")
triple7
((triple8 triple5) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
((triple8 ((triple10) -> (rule6 % int2))) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
((triple8 ((((triple8) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
((((((triple5) -> (rule5 % int3))) -> (rule4 % int2)) triple5) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
((((((triple5) -> (rule5 % int4))) -> (rule4 % int3)) ((triple10) -> (rule6 % int2))) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
Gary is quiet.
("Gary" "is" "quiet" "+")
int4
((((((triple5) -> (rule5 % int5))) -> (rule4 % int4)) ((((triple8) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Gary is red.
("Gary" "is" "red" "+")
int4
Gary is quiet.
("Gary" "is" "quiet" "+")
int5
((((((((triple10) -> (rule6 % int4))) -> (rule5 % int3))) -> (rule4 % int2)) triple5) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Gary is big.
("Gary" "is" "big" "+")
int4
((((((((triple10) -> (rule6 % int4))) -> (rule5 % int3))) -> (rule4 % int2)) ((triple10) -> (rule6 % int4))) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Gary is big.
("Gary" "is" "big" "+")
int4
((((((((triple10) -> (rule6 % int5))) -> (rule5 % int4))) -> (rule4 % int3)) ((((triple8) -> (rule2 % int2))) -> (rule6 % int5))) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
Gary is quiet.
("Gary" "is" "quiet" "+")
int4
Gary is big.
("Gary" "is" "big" "+")
int5
Gary is not rough.
("Gary" "is" "rough" "-")
triple9
Gary is red.
("Gary" "is" "red" "+")
triple8
((((triple5) -> (rule5 % int2))) -> (rule4 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
((((((triple10) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
Gary is round.
("Gary" "is" "round" "+")
triple10
((triple8) -> (rule2 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
((triple8 triple5) -> (rule1 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
((((((triple5) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
((((((triple5) -> (rule5 % int3))) -> (rule4 % int2)) triple5) -> (rule1 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Bob is big.
("Bob" "is" "big" "+")
((triple4) -> (rule6 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
((triple5) -> (rule5 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
((((triple10) -> (rule6 % int2))) -> (rule5 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
((((((triple8) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Bob is quiet.
("Bob" "is" "quiet" "+")
((((triple4) -> (rule6 % int2))) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
((((((triple4) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3