Charlie is big. Charlie is furry. Charlie is kind. Charlie is nice. Charlie is smart. Gary is big. Gary is furry. Gary is green. Gary is kind. Gary is nice. Gary is red. Gary is smart. Red, nice things are green. Green, kind things are red. If something is green then it is nice. Nice, furry things are green. All nice things are red. All furry things are big.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Red, nice things are green.
((("something" "is" "red" "+") ("something" "is" "nice" "+")) -> ("something" "is" "green" "+"))
Green, kind things are red.
((("something" "is" "green" "+") ("something" "is" "kind" "+")) -> ("something" "is" "red" "+"))
If something is green then it is nice.
((("something" "is" "green" "+")) -> ("something" "is" "nice" "+"))
Nice, furry things are green.
((("something" "is" "nice" "+") ("something" "is" "furry" "+")) -> ("something" "is" "green" "+"))
All nice things are red.
((("something" "is" "nice" "+")) -> ("something" "is" "red" "+"))
All furry things are big.
((("something" "is" "furry" "+")) -> ("something" "is" "big" "+"))
Gary is kind.
True
1
proof
[(triple9)]
("Gary" "is" "kind" "+")
triple9
Gary is not green.
False
1
inv-proof
[(triple8 OR ((triple10 triple7) -> rule4) OR ((triple11 triple10) -> rule1) OR ((((triple10) -> rule5) triple10) -> rule1))]
("Gary" "is" "green" "-")
triple8
((triple10 triple7) -> (rule4 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
((triple11 triple10) -> (rule1 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
((((triple10) -> (rule5 % int2)) triple10) -> (rule1 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Charlie is red.
True
2
proof
[(((triple4) -> rule5) OR ((((triple4 triple2) -> rule4) triple3) -> rule2))]
("Charlie" "is" "red" "+")
((triple4) -> (rule5 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
((((triple4 triple2) -> (rule4 % int2)) triple3) -> (rule2 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is not red.
False
2
inv-proof
[(((triple4) -> rule5) OR ((((triple4 triple2) -> rule4) triple3) -> rule2))]
("Charlie" "is" "red" "-")
((triple4) -> (rule5 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
((((triple4 triple2) -> (rule4 % int2)) triple3) -> (rule2 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
@0: Charlie is big.[(triple1 OR ((triple2) -> rule6))] Charlie is furry.[(triple2)] Charlie is kind.[(triple3)] Charlie is nice.[(triple4)] Charlie is smart.[(triple5)] Gary is big.[(triple6 OR ((triple7) -> rule6))] Gary is furry.[(triple7)] Gary is green.[(triple8 OR ((triple10 triple7) -> rule4) OR ((triple11 triple10) -> rule1) OR ((((triple10) -> rule5) triple10) -> rule1))] Gary is kind.[(triple9)] Gary is nice.[(triple10 OR ((triple8) -> rule3))] Gary is red.[(triple11 OR ((triple10) -> rule5) OR ((triple8 triple9) -> rule2) OR ((((triple8) -> rule3)) -> rule5) OR ((((triple10 triple7) -> rule4) triple9) -> rule2))] Gary is smart.[(triple12)] @1: Charlie is green.[(((triple4 triple2) -> rule4) OR ((((triple4) -> rule5) triple4) -> rule1))] Charlie is red.[(((triple4) -> rule5) OR ((((triple4 triple2) -> rule4) triple3) -> rule2))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
((triple2) -> (rule6 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
triple2
Charlie is kind.
("Charlie" "is" "kind" "+")
triple3
Charlie is nice.
("Charlie" "is" "nice" "+")
triple4
Charlie is smart.
("Charlie" "is" "smart" "+")
triple5
Gary is big.
("Gary" "is" "big" "+")
triple6
((triple7) -> (rule6 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
triple7
Gary is green.
("Gary" "is" "green" "+")
triple8
((triple10 triple7) -> (rule4 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
((triple11 triple10) -> (rule1 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
((((triple10) -> (rule5 % int2)) triple10) -> (rule1 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
triple9
Gary is nice.
("Gary" "is" "nice" "+")
triple10
((triple8) -> (rule3 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
triple11
((triple10) -> (rule5 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
((triple8 triple9) -> (rule2 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
((((triple8) -> (rule3 % int2))) -> (rule5 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
((((triple10 triple7) -> (rule4 % int2)) triple9) -> (rule2 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
triple12
Charlie is green.
("Charlie" "is" "green" "+")
((triple4 triple2) -> (rule4 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
((((triple4) -> (rule5 % int2)) triple4) -> (rule1 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
((triple4) -> (rule5 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
((((triple4 triple2) -> (rule4 % int2)) triple3) -> (rule2 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2