Charlie is big. Charlie is green. Charlie is nice. Charlie is quiet. Charlie is round. Charlie is smart. Gary is green. Gary is nice. Gary is quiet. Gary is round. Gary is smart. Gary is white. All smart things are white. If Gary is smart and Gary is nice then Gary is big. All big, smart things are round. All big, round things are green. All nice things are green. Big, green things are nice.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is white.
("Gary" "is" "white" "+")
All smart things are white.
((("something" "is" "smart" "+")) -> ("something" "is" "white" "+"))
If Gary is smart and Gary is nice then Gary is big.
((("Gary" "is" "smart" "+") ("Gary" "is" "nice" "+")) -> ("Gary" "is" "big" "+"))
All big, smart things are round.
((("something" "is" "big" "+") ("something" "is" "smart" "+")) -> ("something" "is" "round" "+"))
All big, round things are green.
((("something" "is" "big" "+") ("something" "is" "round" "+")) -> ("something" "is" "green" "+"))
All nice things are green.
((("something" "is" "nice" "+")) -> ("something" "is" "green" "+"))
Big, green things are nice.
((("something" "is" "big" "+") ("something" "is" "green" "+")) -> ("something" "is" "nice" "+"))
Charlie is round.
True
1
proof
[(triple5 OR ((triple1 triple6) -> rule3))]
("Charlie" "is" "round" "+")
triple5
((triple1 triple6) -> (rule3 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Gary is not white.
False
1
inv-proof
[(triple12 OR ((triple11) -> rule1))]
("Gary" "is" "white" "-")
triple12
((triple11) -> (rule1 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is big.
True
3
proof
[(((triple11 triple8) -> rule2))]
("Gary" "is" "big" "+")
((triple11 triple8) -> (rule2 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is not big.
False
3
inv-proof
[(((triple11 triple8) -> rule2))]
("Gary" "is" "big" "-")
((triple11 triple8) -> (rule2 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
@0: Charlie is big.[(triple1)] Charlie is green.[(triple2 OR ((triple3) -> rule5) OR ((triple1 triple5) -> rule4) OR ((triple1 ((triple1 triple6) -> rule3)) -> rule4))] Charlie is nice.[(triple3 OR ((triple1 triple2) -> rule6) OR ((triple1 ((triple1 triple5) -> rule4)) -> rule6) OR ((triple1 ((triple1 ((triple1 triple6) -> rule3)) -> rule4)) -> rule6))] Charlie is quiet.[(triple4)] Charlie is round.[(triple5 OR ((triple1 triple6) -> rule3))] Charlie is smart.[(triple6)] Gary is green.[(triple7 OR ((triple8) -> rule5) OR ((((triple11 triple8) -> rule2) triple10) -> rule4) OR ((((triple11 triple8) -> rule2) ((((triple11 triple8) -> rule2) triple11) -> rule3)) -> rule4))] Gary is nice.[(triple8)] Gary is quiet.[(triple9)] Gary is round.[(triple10 OR ((((triple11 triple8) -> rule2) triple11) -> rule3))] Gary is smart.[(triple11)] Gary is white.[(triple12 OR ((triple11) -> rule1))] @1: Charlie is white.[(((triple6) -> rule1))] Gary is big.[(((triple11 triple8) -> rule2))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Charlie is green.
("Charlie" "is" "green" "+")
triple2
((triple3) -> (rule5 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
((triple1 triple5) -> (rule4 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
((triple1 ((triple1 triple6) -> (rule3 % int2))) -> (rule4 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
triple3
((triple1 triple2) -> (rule6 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
((triple1 ((triple1 triple5) -> (rule4 % int2))) -> (rule6 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
((triple1 ((triple1 ((triple1 triple6) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple4
Charlie is round.
("Charlie" "is" "round" "+")
triple5
((triple1 triple6) -> (rule3 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
triple6
Gary is green.
("Gary" "is" "green" "+")
triple7
((triple8) -> (rule5 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
((((triple11 triple8) -> (rule2 % int2)) triple10) -> (rule4 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
((((triple11 triple8) -> (rule2 % int3)) ((((triple11 triple8) -> (rule2 % int3)) triple11) -> (rule3 % int2))) -> (rule4 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
Gary is nice.
("Gary" "is" "nice" "+")
triple8
Gary is quiet.
("Gary" "is" "quiet" "+")
triple9
Gary is round.
("Gary" "is" "round" "+")
triple10
((((triple11 triple8) -> (rule2 % int2)) triple11) -> (rule3 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
triple11
Gary is white.
("Gary" "is" "white" "+")
triple12
((triple11) -> (rule1 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
((triple6) -> (rule1 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
((triple11 triple8) -> (rule2 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1