Erin is big. Erin is blue. Erin is cold. Erin is kind. Erin is quiet. Erin is red. Erin is smart. Gary is big. Gary is blue. Gary is cold. Gary is kind. Gary is quiet. Gary is red. Gary is smart. Big people are quiet. Blue, smart people are big. Quiet, big people are blue.
Erin is big.
("Erin" "is" "big" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Big people are quiet.
((("someone" "is" "big" "+")) -> ("someone" "is" "quiet" "+"))
Blue, smart people are big.
((("someone" "is" "blue" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "big" "+"))
Quiet, big people are blue.
((("someone" "is" "quiet" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "blue" "+"))
Erin is cold.
True
1
proof
[(triple3)]
("Erin" "is" "cold" "+")
triple3
Gary is not blue.
False
1
inv-proof
[(triple9 OR ((triple12 triple8) -> rule3) OR ((((triple8) -> rule1) triple8) -> rule3))]
("Gary" "is" "blue" "-")
triple9
((triple12 triple8) -> (rule3 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
((((triple8) -> (rule1 % int2)) triple8) -> (rule3 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
@0: Erin is big.[(triple1 OR ((triple2 triple7) -> rule2))] Erin is blue.[(triple2 OR ((triple5 triple1) -> rule3) OR ((((triple1) -> rule1) triple1) -> rule3))] Erin is cold.[(triple3)] Erin is kind.[(triple4)] Erin is quiet.[(triple5 OR ((triple1) -> rule1) OR ((((triple2 triple7) -> rule2)) -> rule1))] Erin is red.[(triple6)] Erin is smart.[(triple7)] Gary is big.[(triple8 OR ((triple9 triple14) -> rule2))] Gary is blue.[(triple9 OR ((triple12 triple8) -> rule3) OR ((((triple8) -> rule1) triple8) -> rule3))] Gary is cold.[(triple10)] Gary is kind.[(triple11)] Gary is quiet.[(triple12 OR ((triple8) -> rule1) OR ((((triple9 triple14) -> rule2)) -> rule1))] Gary is red.[(triple13)] Gary is smart.[(triple14)]
Erin is big.
("Erin" "is" "big" "+")
triple1
((triple2 triple7) -> (rule2 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
triple2
((triple5 triple1) -> (rule3 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
((((triple1) -> (rule1 % int2)) triple1) -> (rule3 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
triple3
Erin is kind.
("Erin" "is" "kind" "+")
triple4
Erin is quiet.
("Erin" "is" "quiet" "+")
triple5
((triple1) -> (rule1 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
((((triple2 triple7) -> (rule2 % int2))) -> (rule1 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
triple6
Erin is smart.
("Erin" "is" "smart" "+")
triple7
Gary is big.
("Gary" "is" "big" "+")
triple8
((triple9 triple14) -> (rule2 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
triple9
((triple12 triple8) -> (rule3 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
((((triple8) -> (rule1 % int2)) triple8) -> (rule3 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
triple10
Gary is kind.
("Gary" "is" "kind" "+")
triple11
Gary is quiet.
("Gary" "is" "quiet" "+")
triple12
((triple8) -> (rule1 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
((((triple9 triple14) -> (rule2 % int2))) -> (rule1 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
triple13
Gary is smart.
("Gary" "is" "smart" "+")
triple14