Charlie is blue. Charlie is cold. Charlie is nice. Charlie is quiet. Charlie is smart. Gary is big. Gary is blue. Gary is cold. Gary is nice. Gary is quiet. Gary is red. Gary is smart. All big, cold people are red. Cold, nice people are big. If Gary is red and Gary is quiet then Gary is blue.
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is smart.
("Gary" "is" "smart" "+")
All big, cold people are red.
((("someone" "is" "big" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "red" "+"))
Cold, nice people are big.
((("someone" "is" "cold" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "big" "+"))
If Gary is red and Gary is quiet then Gary is blue.
((("Gary" "is" "red" "+") ("Gary" "is" "quiet" "+")) -> ("Gary" "is" "blue" "+"))
Charlie is nice.
True
1
proof
[(triple3)]
("Charlie" "is" "nice" "+")
triple3
Charlie is not blue.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "blue" "-")
triple1
Charlie is big.
True
3
proof
[(((triple2 triple3) -> rule2))]
("Charlie" "is" "big" "+")
((triple2 triple3) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is not big.
False
3
inv-proof
[(((triple2 triple3) -> rule2))]
("Charlie" "is" "big" "-")
((triple2 triple3) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is red.
True
5
proof
[(((((triple2 triple3) -> rule2) triple2) -> rule1))]
("Charlie" "is" "red" "+")
((((triple2 triple3) -> (rule2 % int2)) triple2) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is not red.
False
5
inv-proof
[(((((triple2 triple3) -> rule2) triple2) -> rule1))]
("Charlie" "is" "red" "-")
((((triple2 triple3) -> (rule2 % int2)) triple2) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
@0: Charlie is blue.[(triple1)] Charlie is cold.[(triple2)] Charlie is nice.[(triple3)] Charlie is quiet.[(triple4)] Charlie is smart.[(triple5)] Gary is big.[(triple6 OR ((triple8 triple9) -> rule2))] Gary is blue.[(triple7 OR ((triple11 triple10) -> rule3) OR ((((triple6 triple8) -> rule1) triple10) -> rule3) OR ((((((triple8 triple9) -> rule2) triple8) -> rule1) triple10) -> rule3))] Gary is cold.[(triple8)] Gary is nice.[(triple9)] Gary is quiet.[(triple10)] Gary is red.[(triple11 OR ((triple6 triple8) -> rule1) OR ((((triple8 triple9) -> rule2) triple8) -> rule1))] Gary is smart.[(triple12)] @1: Charlie is big.[(((triple2 triple3) -> rule2))] @2: Charlie is red.[(((((triple2 triple3) -> rule2) triple2) -> rule1))]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
Charlie is cold.
("Charlie" "is" "cold" "+")
triple2
Charlie is nice.
("Charlie" "is" "nice" "+")
triple3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple4
Charlie is smart.
("Charlie" "is" "smart" "+")
triple5
Gary is big.
("Gary" "is" "big" "+")
triple6
((triple8 triple9) -> (rule2 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
triple7
((triple11 triple10) -> (rule3 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
((((triple6 triple8) -> (rule1 % int2)) triple10) -> (rule3 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
((((((triple8 triple9) -> (rule2 % int3)) triple8) -> (rule1 % int2)) triple10) -> (rule3 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
Gary is cold.
("Gary" "is" "cold" "+")
triple8
Gary is nice.
("Gary" "is" "nice" "+")
triple9
Gary is quiet.
("Gary" "is" "quiet" "+")
triple10
Gary is red.
("Gary" "is" "red" "+")
triple11
((triple6 triple8) -> (rule1 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
((((triple8 triple9) -> (rule2 % int2)) triple8) -> (rule1 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
triple12
Charlie is big.
("Charlie" "is" "big" "+")
((triple2 triple3) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
((((triple2 triple3) -> (rule2 % int2)) triple2) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2