Charlie is cold. Charlie is furry. Charlie is quiet. Charlie is rough. Charlie is smart. Charlie is not white. Erin is blue. Erin is cold. Erin is furry. Erin is rough. Erin is smart. Erin is white. If something is furry then it is quiet. If Charlie is white and Charlie is rough then Charlie is not furry. If something is quiet then it is rough. If something is rough and not white then it is blue. All rough things are smart. If something is rough then it is cold.
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is not white.
("Charlie" "is" "white" "-")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is white.
("Erin" "is" "white" "+")
If something is furry then it is quiet.
((("something" "is" "furry" "+")) -> ("something" "is" "quiet" "+"))
If Charlie is white and Charlie is rough then Charlie is not furry.
((("Charlie" "is" "white" "+") ("Charlie" "is" "rough" "+")) -> ("Charlie" "is" "furry" "-"))
If something is quiet then it is rough.
((("something" "is" "quiet" "+")) -> ("something" "is" "rough" "+"))
If something is rough and not white then it is blue.
((("something" "is" "rough" "+") ("something" "is" "white" "~")) -> ("something" "is" "blue" "+"))
All rough things are smart.
((("something" "is" "rough" "+")) -> ("something" "is" "smart" "+"))
If something is rough then it is cold.
((("something" "is" "rough" "+")) -> ("something" "is" "cold" "+"))
Erin is smart.
True
1
proof
[(triple11 OR ((triple10) -> rule5) OR ((((((triple9) -> rule1)) -> rule3)) -> rule5))]
("Erin" "is" "smart" "+")
triple11
((triple10) -> (rule5 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
((((((triple9) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
Erin is not furry.
False
1
inv-proof
[(triple9)]
("Erin" "is" "furry" "-")
triple9
@0: Charlie is cold.[(triple1 OR ((triple4) -> rule6) OR ((((triple3) -> rule3)) -> rule6) OR ((((((triple2) -> rule1)) -> rule3)) -> rule6))] Charlie is furry.[(triple2)] Charlie is not white.[(triple6)] Charlie is quiet.[(triple3 OR ((triple2) -> rule1))] Charlie is rough.[(triple4 OR ((triple3) -> rule3) OR ((((triple2) -> rule1)) -> rule3))] Charlie is smart.[(triple5 OR ((triple4) -> rule5) OR ((((triple3) -> rule3)) -> rule5) OR ((((((triple2) -> rule1)) -> rule3)) -> rule5))] Erin is blue.[(triple7)] Erin is cold.[(triple8 OR ((triple10) -> rule6) OR ((((((triple9) -> rule1)) -> rule3)) -> rule6))] Erin is furry.[(triple9)] Erin is rough.[(triple10 OR ((((triple9) -> rule1)) -> rule3))] Erin is smart.[(triple11 OR ((triple10) -> rule5) OR ((((((triple9) -> rule1)) -> rule3)) -> rule5))] Erin is white.[(triple12)] @1: Charlie is blue.[(((triple4 triple6) -> rule4) OR ((((triple3) -> rule3) triple6) -> rule4) OR ((((((triple2) -> rule1)) -> rule3) triple6) -> rule4))] Erin is quiet.[(((triple9) -> rule1))]
Charlie is cold.
("Charlie" "is" "cold" "+")
triple1
((triple4) -> (rule6 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
((((triple3) -> (rule3 % int2))) -> (rule6 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
((((((triple2) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Charlie is furry.
("Charlie" "is" "furry" "+")
triple2
Charlie is not white.
("Charlie" "is" "white" "-")
triple6
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple3
((triple2) -> (rule1 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
triple4
((triple3) -> (rule3 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
triple5
((triple4) -> (rule5 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
((((triple3) -> (rule3 % int2))) -> (rule5 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
((((((triple2) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Erin is blue.
("Erin" "is" "blue" "+")
triple7
Erin is cold.
("Erin" "is" "cold" "+")
triple8
((triple10) -> (rule6 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
((((((triple9) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
Erin is furry.
("Erin" "is" "furry" "+")
triple9
Erin is rough.
("Erin" "is" "rough" "+")
triple10
((((triple9) -> (rule1 % int2))) -> (rule3 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
triple11
((triple10) -> (rule5 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
((((((triple9) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
Erin is white.
("Erin" "is" "white" "+")
triple12
Charlie is blue.
("Charlie" "is" "blue" "+")
((triple4 triple6) -> (rule4 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
((((triple3) -> (rule3 % int2)) triple6) -> (rule4 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
((((((triple2) -> (rule1 % int3))) -> (rule3 % int2)) triple6) -> (rule4 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Erin is quiet.
("Erin" "is" "quiet" "+")
((triple9) -> (rule1 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1