Charlie is cold. Charlie is green. Charlie is kind. Charlie is quiet. Charlie is round. Erin is cold. Erin is green. Erin is kind. Erin is quiet. Erin is round. Round things are green. Round things are white. All quiet things are green. If something is round then it is blue. Cold things are round. If Charlie is round then Charlie is quiet. If Erin is green and Erin is quiet then Erin is cold. If Charlie is cold then Charlie is white.
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 round.
("Charlie" "is" "round" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is round.
("Erin" "is" "round" "+")
Round things are green.
((("something" "is" "round" "+")) -> ("something" "is" "green" "+"))
Round things are white.
((("something" "is" "round" "+")) -> ("something" "is" "white" "+"))
All quiet things are green.
((("something" "is" "quiet" "+")) -> ("something" "is" "green" "+"))
If something is round then it is blue.
((("something" "is" "round" "+")) -> ("something" "is" "blue" "+"))
Cold things are round.
((("something" "is" "cold" "+")) -> ("something" "is" "round" "+"))
If Charlie is round then Charlie is quiet.
((("Charlie" "is" "round" "+")) -> ("Charlie" "is" "quiet" "+"))
If Erin is green and Erin is quiet then Erin is cold.
((("Erin" "is" "green" "+") ("Erin" "is" "quiet" "+")) -> ("Erin" "is" "cold" "+"))
If Charlie is cold then Charlie is white.
((("Charlie" "is" "cold" "+")) -> ("Charlie" "is" "white" "+"))
Erin is quiet.
True
1
proof
[(triple9)]
("Erin" "is" "quiet" "+")
triple9
Erin is not quiet.
False
1
inv-proof
[(triple9)]
("Erin" "is" "quiet" "-")
triple9
@0: Charlie is cold.[(triple1)] Charlie is green.[(triple2 OR ((triple4) -> rule3) OR ((triple5) -> rule1) OR ((((triple1) -> rule5)) -> rule1) OR ((((triple5) -> rule6)) -> rule3) OR ((((((triple1) -> rule5)) -> rule6)) -> rule3))] Charlie is kind.[(triple3)] Charlie is quiet.[(triple4 OR ((triple5) -> rule6) OR ((((triple1) -> rule5)) -> rule6))] Charlie is round.[(triple5 OR ((triple1) -> rule5))] Erin is cold.[(triple6 OR ((triple7 triple9) -> rule7) OR ((((triple10) -> rule1) triple9) -> rule7) OR ((((triple9) -> rule3) triple9) -> rule7))] Erin is green.[(triple7 OR ((triple10) -> rule1) OR ((triple9) -> rule3) OR ((((triple6) -> rule5)) -> rule1))] Erin is kind.[(triple8)] Erin is quiet.[(triple9)] Erin is round.[(triple10 OR ((triple6) -> rule5) OR ((((triple7 triple9) -> rule7)) -> rule5) OR ((((((triple9) -> rule3) triple9) -> rule7)) -> rule5))] @1: Charlie is blue.[(((triple5) -> rule4) OR ((((triple1) -> rule5)) -> rule4))] Charlie is white.[(((triple1) -> rule8) OR ((triple5) -> rule2) OR ((((triple1) -> rule5)) -> rule2))] Erin is blue.[(((triple10) -> rule4) OR ((((triple6) -> rule5)) -> rule4) OR ((((((triple7 triple9) -> rule7)) -> rule5)) -> rule4) OR ((((((((triple9) -> rule3) triple9) -> rule7)) -> rule5)) -> rule4))] Erin is white.[(((triple10) -> rule2) OR ((((triple6) -> rule5)) -> rule2) OR ((((((triple7 triple9) -> rule7)) -> rule5)) -> rule2) OR ((((((((triple9) -> rule3) triple9) -> rule7)) -> rule5)) -> rule2))]
Charlie is cold.
("Charlie" "is" "cold" "+")
triple1
Charlie is green.
("Charlie" "is" "green" "+")
triple2
((triple4) -> (rule3 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
((triple5) -> (rule1 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
((((triple1) -> (rule5 % int2))) -> (rule1 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
((((triple5) -> (rule6 % int2))) -> (rule3 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
((((((triple1) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
Charlie is kind.
("Charlie" "is" "kind" "+")
triple3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple4
((triple5) -> (rule6 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
((((triple1) -> (rule5 % int2))) -> (rule6 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
triple5
((triple1) -> (rule5 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
triple6
((triple7 triple9) -> (rule7 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
((((triple10) -> (rule1 % int2)) triple9) -> (rule7 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
((((triple9) -> (rule3 % int2)) triple9) -> (rule7 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
triple7
((triple10) -> (rule1 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
((triple9) -> (rule3 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
((((triple6) -> (rule5 % int2))) -> (rule1 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
triple8
Erin is quiet.
("Erin" "is" "quiet" "+")
triple9
Erin is round.
("Erin" "is" "round" "+")
triple10
((triple6) -> (rule5 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
((((triple7 triple9) -> (rule7 % int2))) -> (rule5 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
((((((triple9) -> (rule3 % int3)) triple9) -> (rule7 % int2))) -> (rule5 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Charlie is blue.
("Charlie" "is" "blue" "+")
((triple5) -> (rule4 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
((((triple1) -> (rule5 % int2))) -> (rule4 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
((triple1) -> (rule8 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
((triple5) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
((((triple1) -> (rule5 % int2))) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
((triple10) -> (rule4 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
((((triple6) -> (rule5 % int2))) -> (rule4 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
((((((triple7 triple9) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
((((((((triple9) -> (rule3 % int4)) triple9) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Erin is green.
("Erin" "is" "green" "+")
int4
Erin is white.
("Erin" "is" "white" "+")
((triple10) -> (rule2 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
((((triple6) -> (rule5 % int2))) -> (rule2 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
((((((triple7 triple9) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
((((((((triple9) -> (rule3 % int4)) triple9) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Erin is green.
("Erin" "is" "green" "+")
int4