Charlie is big. Charlie is green. Charlie is kind. Charlie is nice. Charlie is red. Charlie is smart. Charlie is white. Harry is kind. Harry is smart. Harry is white. All smart, big things are nice. If something is smart and white then it is big. All green things are big. If Harry is nice then Harry is white. If something is nice then it is red. If something is green and smart then it is red.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is white.
("Harry" "is" "white" "+")
All smart, big things are nice.
((("something" "is" "smart" "+") ("something" "is" "big" "+")) -> ("something" "is" "nice" "+"))
If something is smart and white then it is big.
((("something" "is" "smart" "+") ("something" "is" "white" "+")) -> ("something" "is" "big" "+"))
All green things are big.
((("something" "is" "green" "+")) -> ("something" "is" "big" "+"))
If Harry is nice then Harry is white.
((("Harry" "is" "nice" "+")) -> ("Harry" "is" "white" "+"))
If something is nice then it is red.
((("something" "is" "nice" "+")) -> ("something" "is" "red" "+"))
If something is green and smart then it is red.
((("something" "is" "green" "+") ("something" "is" "smart" "+")) -> ("something" "is" "red" "+"))
Charlie is kind.
True
1
proof
[(triple3)]
("Charlie" "is" "kind" "+")
triple3
Harry is not kind.
False
1
inv-proof
[(triple8)]
("Harry" "is" "kind" "-")
triple8
Harry is big.
True
3
proof
[(((triple9 triple10) -> rule2))]
("Harry" "is" "big" "+")
((triple9 triple10) -> (rule2 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is not big.
False
3
inv-proof
[(((triple9 triple10) -> rule2))]
("Harry" "is" "big" "-")
((triple9 triple10) -> (rule2 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is nice.
True
5
proof
[(((triple9 ((triple9 triple10) -> rule2)) -> rule1))]
("Harry" "is" "nice" "+")
((triple9 ((triple9 triple10) -> (rule2 % int2))) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is not nice.
False
5
inv-proof
[(((triple9 ((triple9 triple10) -> rule2)) -> rule1))]
("Harry" "is" "nice" "-")
((triple9 ((triple9 triple10) -> (rule2 % int2))) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is red.
True
6
proof
[(((((triple9 ((triple9 triple10) -> rule2)) -> rule1)) -> rule5))]
("Harry" "is" "red" "+")
((((triple9 ((triple9 triple10) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Harry is not red.
False
6
inv-proof
[(((((triple9 ((triple9 triple10) -> rule2)) -> rule1)) -> rule5))]
("Harry" "is" "red" "-")
((((triple9 ((triple9 triple10) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
@0: Charlie is big.[(triple1 OR ((triple2) -> rule3) OR ((triple6 triple7) -> rule2))] Charlie is green.[(triple2)] Charlie is kind.[(triple3)] Charlie is nice.[(triple4 OR ((triple6 triple1) -> rule1) OR ((triple6 ((triple2) -> rule3)) -> rule1) OR ((triple6 ((triple6 triple7) -> rule2)) -> rule1))] Charlie is red.[(triple5 OR ((triple4) -> rule5) OR ((triple2 triple6) -> rule6) OR ((((triple6 triple1) -> rule1)) -> rule5) OR ((((triple6 ((triple2) -> rule3)) -> rule1)) -> rule5) OR ((((triple6 ((triple6 triple7) -> rule2)) -> rule1)) -> rule5))] Charlie is smart.[(triple6)] Charlie is white.[(triple7)] Harry is kind.[(triple8)] Harry is smart.[(triple9)] Harry is white.[(triple10)] @1: Harry is big.[(((triple9 triple10) -> rule2))] @2: Harry is nice.[(((triple9 ((triple9 triple10) -> rule2)) -> rule1))] @3: Harry is red.[(((((triple9 ((triple9 triple10) -> rule2)) -> rule1)) -> rule5))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
((triple2) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
((triple6 triple7) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
triple2
Charlie is kind.
("Charlie" "is" "kind" "+")
triple3
Charlie is nice.
("Charlie" "is" "nice" "+")
triple4
((triple6 triple1) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
((triple6 ((triple2) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
((triple6 ((triple6 triple7) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
triple5
((triple4) -> (rule5 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
((triple2 triple6) -> (rule6 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
((((triple6 triple1) -> (rule1 % int2))) -> (rule5 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
((((triple6 ((triple2) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
((((triple6 ((triple6 triple7) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Charlie is smart.
("Charlie" "is" "smart" "+")
triple6
Charlie is white.
("Charlie" "is" "white" "+")
triple7
Harry is kind.
("Harry" "is" "kind" "+")
triple8
Harry is smart.
("Harry" "is" "smart" "+")
triple9
Harry is white.
("Harry" "is" "white" "+")
triple10
Harry is big.
("Harry" "is" "big" "+")
((triple9 triple10) -> (rule2 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
((triple9 ((triple9 triple10) -> (rule2 % int2))) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
((((triple9 ((triple9 triple10) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3