Charlie is cold. Charlie is green. Charlie is kind. Charlie is quiet. Charlie is red. Charlie is white. Charlie is young. Erin is green. Erin is kind. Erin is quiet. Erin is white. Erin is young. If Charlie is cold then Charlie is green. Young things are cold. Cold things are young. Red, cold things are white. If something is kind and young then it is green. All kind things are green.
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is white.
("Erin" "is" "white" "+")
Erin is young.
("Erin" "is" "young" "+")
If Charlie is cold then Charlie is green.
((("Charlie" "is" "cold" "+")) -> ("Charlie" "is" "green" "+"))
Young things are cold.
((("something" "is" "young" "+")) -> ("something" "is" "cold" "+"))
Cold things are young.
((("something" "is" "cold" "+")) -> ("something" "is" "young" "+"))
Red, cold things are white.
((("something" "is" "red" "+") ("something" "is" "cold" "+")) -> ("something" "is" "white" "+"))
If something is kind and young then it is green.
((("something" "is" "kind" "+") ("something" "is" "young" "+")) -> ("something" "is" "green" "+"))
All kind things are green.
((("something" "is" "kind" "+")) -> ("something" "is" "green" "+"))
Charlie is young.
True
1
proof
[(triple7 OR ((triple1) -> rule3))]
("Charlie" "is" "young" "+")
triple7
((triple1) -> (rule3 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is not quiet.
False
1
inv-proof
[(triple4)]
("Charlie" "is" "quiet" "-")
triple4
@0: Charlie is cold.[(triple1 OR ((triple7) -> rule2))] Charlie is green.[(triple2 OR ((triple1) -> rule1) OR ((triple3) -> rule6) OR ((triple3 triple7) -> rule5) OR ((((triple7) -> rule2)) -> rule1) OR ((triple3 ((triple1) -> rule3)) -> rule5))] Charlie is kind.[(triple3)] Charlie is quiet.[(triple4)] Charlie is red.[(triple5)] Charlie is white.[(triple6 OR ((triple5 triple1) -> rule4) OR ((triple5 ((triple7) -> rule2)) -> rule4))] Charlie is young.[(triple7 OR ((triple1) -> rule3))] Erin is green.[(triple8 OR ((triple9) -> rule6) OR ((triple9 triple12) -> rule5))] Erin is kind.[(triple9)] Erin is quiet.[(triple10)] Erin is white.[(triple11)] Erin is young.[(triple12)] @1: Erin is cold.[(((triple12) -> rule2))]
Charlie is cold.
("Charlie" "is" "cold" "+")
triple1
((triple7) -> (rule2 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
triple2
((triple1) -> (rule1 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
((triple3) -> (rule6 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
((triple3 triple7) -> (rule5 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
((((triple7) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
((triple3 ((triple1) -> (rule3 % int2))) -> (rule5 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
triple3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple4
Charlie is red.
("Charlie" "is" "red" "+")
triple5
Charlie is white.
("Charlie" "is" "white" "+")
triple6
((triple5 triple1) -> (rule4 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
((triple5 ((triple7) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
triple7
((triple1) -> (rule3 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
triple8
((triple9) -> (rule6 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
((triple9 triple12) -> (rule5 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
triple9
Erin is quiet.
("Erin" "is" "quiet" "+")
triple10
Erin is white.
("Erin" "is" "white" "+")
triple11
Erin is young.
("Erin" "is" "young" "+")
triple12
Erin is cold.
("Erin" "is" "cold" "+")
((triple12) -> (rule2 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1