Charlie is blue. Charlie is cold. Charlie is green. Charlie is nice. Charlie is quiet. Charlie is round. Erin is cold. Erin is green. Erin is nice. Erin is quiet. Erin is red. Erin is round. If something is green and blue then it is red. If something is red then it is cold. If something is red and round then it is nice.
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is round.
("Erin" "is" "round" "+")
If something is green and blue then it is red.
((("something" "is" "green" "+") ("something" "is" "blue" "+")) -> ("something" "is" "red" "+"))
If something is red then it is cold.
((("something" "is" "red" "+")) -> ("something" "is" "cold" "+"))
If something is red and round then it is nice.
((("something" "is" "red" "+") ("something" "is" "round" "+")) -> ("something" "is" "nice" "+"))
Charlie is cold.
True
1
proof
[(triple2 OR ((((triple3 triple1) -> rule1)) -> rule2))]
("Charlie" "is" "cold" "+")
triple2
((((triple3 triple1) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Erin is not cold.
False
1
inv-proof
[(triple7 OR ((triple11) -> rule2))]
("Erin" "is" "cold" "-")
triple7
((triple11) -> (rule2 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
@0: Charlie is blue.[(triple1)] Charlie is cold.[(triple2 OR ((((triple3 triple1) -> rule1)) -> rule2))] Charlie is green.[(triple3)] Charlie is nice.[(triple4 OR ((((triple3 triple1) -> rule1) triple6) -> rule3))] Charlie is quiet.[(triple5)] Charlie is round.[(triple6)] Erin is cold.[(triple7 OR ((triple11) -> rule2))] Erin is green.[(triple8)] Erin is nice.[(triple9 OR ((triple11 triple12) -> rule3))] Erin is quiet.[(triple10)] Erin is red.[(triple11)] Erin is round.[(triple12)] @1: Charlie is red.[(((triple3 triple1) -> rule1))]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
Charlie is cold.
("Charlie" "is" "cold" "+")
triple2
((((triple3 triple1) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
triple3
Charlie is nice.
("Charlie" "is" "nice" "+")
triple4
((((triple3 triple1) -> (rule1 % int2)) triple6) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple5
Charlie is round.
("Charlie" "is" "round" "+")
triple6
Erin is cold.
("Erin" "is" "cold" "+")
triple7
((triple11) -> (rule2 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
triple8
Erin is nice.
("Erin" "is" "nice" "+")
triple9
((triple11 triple12) -> (rule3 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
triple10
Erin is red.
("Erin" "is" "red" "+")
triple11
Erin is round.
("Erin" "is" "round" "+")
triple12
Charlie is red.
("Charlie" "is" "red" "+")
((triple3 triple1) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1