Bob is big. Bob is green. Bob is kind. Bob is nice. Bob is white. Charlie is big. Charlie is furry. Charlie is green. Charlie is kind. Charlie is nice. Charlie is smart. Charlie is white. Harry is big. Harry is green. Harry is nice. Harry is smart. Kind, big things are furry. All kind, white things are green. All green things are kind. Nice, green things are smart. If Bob is big and Bob is white then Bob is smart. If something is furry then it is white.
Bob is big.
("Bob" "is" "big" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is white.
("Bob" "is" "white" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Kind, big things are furry.
((("something" "is" "kind" "+") ("something" "is" "big" "+")) -> ("something" "is" "furry" "+"))
All kind, white things are green.
((("something" "is" "kind" "+") ("something" "is" "white" "+")) -> ("something" "is" "green" "+"))
All green things are kind.
((("something" "is" "green" "+")) -> ("something" "is" "kind" "+"))
Nice, green things are smart.
((("something" "is" "nice" "+") ("something" "is" "green" "+")) -> ("something" "is" "smart" "+"))
If Bob is big and Bob is white then Bob is smart.
((("Bob" "is" "big" "+") ("Bob" "is" "white" "+")) -> ("Bob" "is" "smart" "+"))
If something is furry then it is white.
((("something" "is" "furry" "+")) -> ("something" "is" "white" "+"))
Harry is green.
True
1
proof
[(triple14)]
("Harry" "is" "green" "+")
triple14
Charlie is not furry.
False
1
inv-proof
[(triple7 OR ((triple9 triple6) -> rule1) OR ((((triple8) -> rule3) triple6) -> rule1))]
("Charlie" "is" "furry" "-")
triple7
((triple9 triple6) -> (rule1 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
((((triple8) -> (rule3 % int2)) triple6) -> (rule1 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Bob is furry.
True
3
proof
[(((triple3 triple1) -> rule1) OR ((((triple2) -> rule3) triple1) -> rule1))]
("Bob" "is" "furry" "+")
((triple3 triple1) -> (rule1 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
((((triple2) -> (rule3 % int2)) triple1) -> (rule1 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is not smart.
False
3
inv-proof
[(((triple1 triple5) -> rule5) OR ((triple4 triple2) -> rule4) OR ((triple4 ((triple3 triple5) -> rule2)) -> rule4) OR ((triple1 ((((triple3 triple1) -> rule1)) -> rule6)) -> rule5) OR ((triple1 ((((((triple2) -> rule3) triple1) -> rule1)) -> rule6)) -> rule5) OR ((triple4 ((triple3 ((((triple3 triple1) -> rule1)) -> rule6)) -> rule2)) -> rule4))]
("Bob" "is" "smart" "-")
((triple1 triple5) -> (rule5 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
((triple4 triple2) -> (rule4 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
((triple4 ((triple3 triple5) -> (rule2 % int2))) -> (rule4 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
((triple1 ((((triple3 triple1) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
((triple1 ((((((triple2) -> (rule3 % int4)) triple1) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Bob is kind.
("Bob" "is" "kind" "+")
int4
((triple4 ((triple3 ((((triple3 triple1) -> (rule1 % int4))) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is furry.
("Bob" "is" "furry" "+")
int4
Harry is furry.
True
4
proof
[(((((triple14) -> rule3) triple13) -> rule1))]
("Harry" "is" "furry" "+")
((((triple14) -> (rule3 % int2)) triple13) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is not furry.
False
4
inv-proof
[(((((triple14) -> rule3) triple13) -> rule1))]
("Harry" "is" "furry" "-")
((((triple14) -> (rule3 % int2)) triple13) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is white.
True
5
proof
[(((((((triple14) -> rule3) triple13) -> rule1)) -> rule6))]
("Harry" "is" "white" "+")
((((((triple14) -> (rule3 % int3)) triple13) -> (rule1 % int2))) -> (rule6 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
Harry is not white.
False
5
inv-proof
[(((((((triple14) -> rule3) triple13) -> rule1)) -> rule6))]
("Harry" "is" "white" "-")
((((((triple14) -> (rule3 % int3)) triple13) -> (rule1 % int2))) -> (rule6 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
@0: Bob is big.[(triple1)] Bob is green.[(triple2 OR ((triple3 triple5) -> rule2) OR ((triple3 ((((triple3 triple1) -> rule1)) -> rule6)) -> rule2))] Bob is kind.[(triple3 OR ((triple2) -> rule3))] Bob is nice.[(triple4)] Bob is white.[(triple5 OR ((((triple3 triple1) -> rule1)) -> rule6) OR ((((((triple2) -> rule3) triple1) -> rule1)) -> rule6))] Charlie is big.[(triple6)] Charlie is furry.[(triple7 OR ((triple9 triple6) -> rule1) OR ((((triple8) -> rule3) triple6) -> rule1))] Charlie is green.[(triple8 OR ((triple9 triple12) -> rule2) OR ((triple9 ((triple7) -> rule6)) -> rule2) OR ((triple9 ((((triple9 triple6) -> rule1)) -> rule6)) -> rule2))] Charlie is kind.[(triple9 OR ((triple8) -> rule3))] Charlie is nice.[(triple10)] Charlie is smart.[(triple11 OR ((triple10 triple8) -> rule4) OR ((triple10 ((triple9 triple12) -> rule2)) -> rule4) OR ((triple10 ((triple9 ((triple7) -> rule6)) -> rule2)) -> rule4) OR ((triple10 ((triple9 ((((triple9 triple6) -> rule1)) -> rule6)) -> rule2)) -> rule4))] Charlie is white.[(triple12 OR ((triple7) -> rule6) OR ((((triple9 triple6) -> rule1)) -> rule6) OR ((((((triple8) -> rule3) triple6) -> rule1)) -> rule6))] Harry is big.[(triple13)] Harry is green.[(triple14)] Harry is nice.[(triple15)] Harry is smart.[(triple16 OR ((triple15 triple14) -> rule4))] @1: Bob is furry.[(((triple3 triple1) -> rule1) OR ((((triple2) -> rule3) triple1) -> rule1))] Bob is smart.[(((triple1 triple5) -> rule5) OR ((triple4 triple2) -> rule4) OR ((triple4 ((triple3 triple5) -> rule2)) -> rule4) OR ((triple1 ((((triple3 triple1) -> rule1)) -> rule6)) -> rule5) OR ((triple1 ((((((triple2) -> rule3) triple1) -> rule1)) -> rule6)) -> rule5) OR ((triple4 ((triple3 ((((triple3 triple1) -> rule1)) -> rule6)) -> rule2)) -> rule4))] Harry is kind.[(((triple14) -> rule3))] @2: Harry is furry.[(((((triple14) -> rule3) triple13) -> rule1))] @3: Harry is white.[(((((((triple14) -> rule3) triple13) -> rule1)) -> rule6))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is green.
("Bob" "is" "green" "+")
triple2
((triple3 triple5) -> (rule2 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
((triple3 ((((triple3 triple1) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Bob is kind.
("Bob" "is" "kind" "+")
triple3
((triple2) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
triple4
Bob is white.
("Bob" "is" "white" "+")
triple5
((((triple3 triple1) -> (rule1 % int2))) -> (rule6 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
((((((triple2) -> (rule3 % int3)) triple1) -> (rule1 % int2))) -> (rule6 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
Charlie is big.
("Charlie" "is" "big" "+")
triple6
Charlie is furry.
("Charlie" "is" "furry" "+")
triple7
((triple9 triple6) -> (rule1 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
((((triple8) -> (rule3 % int2)) triple6) -> (rule1 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
triple8
((triple9 triple12) -> (rule2 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
((triple9 ((triple7) -> (rule6 % int2))) -> (rule2 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
((triple9 ((((triple9 triple6) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
Charlie is kind.
("Charlie" "is" "kind" "+")
triple9
((triple8) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
triple10
Charlie is smart.
("Charlie" "is" "smart" "+")
triple11
((triple10 triple8) -> (rule4 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
((triple10 ((triple9 triple12) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
((triple10 ((triple9 ((triple7) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
((triple10 ((triple9 ((((triple9 triple6) -> (rule1 % int4))) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
Charlie is furry.
("Charlie" "is" "furry" "+")
int4
Charlie is white.
("Charlie" "is" "white" "+")
triple12
((triple7) -> (rule6 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
((((triple9 triple6) -> (rule1 % int2))) -> (rule6 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
((((((triple8) -> (rule3 % int3)) triple6) -> (rule1 % int2))) -> (rule6 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Harry is big.
("Harry" "is" "big" "+")
triple13
Harry is green.
("Harry" "is" "green" "+")
triple14
Harry is nice.
("Harry" "is" "nice" "+")
triple15
Harry is smart.
("Harry" "is" "smart" "+")
triple16
((triple15 triple14) -> (rule4 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
((triple3 triple1) -> (rule1 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
((((triple2) -> (rule3 % int2)) triple1) -> (rule1 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
((triple1 triple5) -> (rule5 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
((triple4 triple2) -> (rule4 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
((triple4 ((triple3 triple5) -> (rule2 % int2))) -> (rule4 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
((triple1 ((((triple3 triple1) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
((triple1 ((((((triple2) -> (rule3 % int4)) triple1) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Bob is kind.
("Bob" "is" "kind" "+")
int4
((triple4 ((triple3 ((((triple3 triple1) -> (rule1 % int4))) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is furry.
("Bob" "is" "furry" "+")
int4
Harry is kind.
("Harry" "is" "kind" "+")
((triple14) -> (rule3 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
((((triple14) -> (rule3 % int2)) triple13) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
((((((triple14) -> (rule3 % int3)) triple13) -> (rule1 % int2))) -> (rule6 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3