Anne is cold. Anne is green. Anne is red. Anne is rough. Anne is smart. Anne is white. Anne is young. Charlie is rough. Charlie is white. Charlie is young. All rough people are smart. If someone is rough then they are cold. Smart, green people are rough. All cold people are red. If someone is cold and red then they are rough. Red people are green.
Anne is cold.
("Anne" "is" "cold" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Anne is white.
("Anne" "is" "white" "+")
Anne is young.
("Anne" "is" "young" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Charlie is young.
("Charlie" "is" "young" "+")
All rough people are smart.
((("someone" "is" "rough" "+")) -> ("someone" "is" "smart" "+"))
If someone is rough then they are cold.
((("someone" "is" "rough" "+")) -> ("someone" "is" "cold" "+"))
Smart, green people are rough.
((("someone" "is" "smart" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "rough" "+"))
All cold people are red.
((("someone" "is" "cold" "+")) -> ("someone" "is" "red" "+"))
If someone is cold and red then they are rough.
((("someone" "is" "cold" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "rough" "+"))
Red people are green.
((("someone" "is" "red" "+")) -> ("someone" "is" "green" "+"))
Charlie is rough.
True
1
proof
[(triple8)]
("Charlie" "is" "rough" "+")
triple8
Anne is not red.
False
1
inv-proof
[(triple3 OR ((triple1) -> rule4) OR ((((triple4) -> rule2)) -> rule4) OR ((((((triple5 triple2) -> rule3)) -> rule2)) -> rule4))]
("Anne" "is" "red" "-")
triple3
((triple1) -> (rule4 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
((((triple4) -> (rule2 % int2))) -> (rule4 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
((((((triple5 triple2) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
Charlie is cold.
True
2
proof
[(((triple8) -> rule2))]
("Charlie" "is" "cold" "+")
((triple8) -> (rule2 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is not smart.
False
2
inv-proof
[(((triple8) -> rule1))]
("Charlie" "is" "smart" "-")
((triple8) -> (rule1 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is red.
True
3
proof
[(((((triple8) -> rule2)) -> rule4))]
("Charlie" "is" "red" "+")
((((triple8) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is not red.
False
3
inv-proof
[(((((triple8) -> rule2)) -> rule4))]
("Charlie" "is" "red" "-")
((((triple8) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is green.
True
4
proof
[(((((((triple8) -> rule2)) -> rule4)) -> rule6))]
("Charlie" "is" "green" "+")
((((((triple8) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
Charlie is not green.
False
4
inv-proof
[(((((((triple8) -> rule2)) -> rule4)) -> rule6))]
("Charlie" "is" "green" "-")
((((((triple8) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
@0: Anne is cold.[(triple1 OR ((triple4) -> rule2) OR ((((triple5 triple2) -> rule3)) -> rule2) OR ((((triple5 ((triple3) -> rule6)) -> rule3)) -> rule2))] Anne is green.[(triple2 OR ((triple3) -> rule6) OR ((((triple1) -> rule4)) -> rule6) OR ((((((triple4) -> rule2)) -> rule4)) -> rule6))] Anne is red.[(triple3 OR ((triple1) -> rule4) OR ((((triple4) -> rule2)) -> rule4) OR ((((((triple5 triple2) -> rule3)) -> rule2)) -> rule4))] Anne is rough.[(triple4 OR ((triple1 triple3) -> rule5) OR ((triple5 triple2) -> rule3) OR ((triple1 ((triple1) -> rule4)) -> rule5) OR ((triple5 ((triple3) -> rule6)) -> rule3) OR ((triple5 ((((triple1) -> rule4)) -> rule6)) -> rule3))] Anne is smart.[(triple5 OR ((triple4) -> rule1) OR ((((triple1 triple3) -> rule5)) -> rule1) OR ((((triple1 ((triple1) -> rule4)) -> rule5)) -> rule1))] Anne is white.[(triple6)] Anne is young.[(triple7)] Charlie is rough.[(triple8)] Charlie is white.[(triple9)] Charlie is young.[(triple10)] @1: Charlie is cold.[(((triple8) -> rule2))] Charlie is smart.[(((triple8) -> rule1))] @2: Charlie is red.[(((((triple8) -> rule2)) -> rule4))] @3: Charlie is green.[(((((((triple8) -> rule2)) -> rule4)) -> rule6))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
((triple4) -> (rule2 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
((((triple5 triple2) -> (rule3 % int2))) -> (rule2 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
((((triple5 ((triple3) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Anne is green.
("Anne" "is" "green" "+")
triple2
((triple3) -> (rule6 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
((((triple1) -> (rule4 % int2))) -> (rule6 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
((((((triple4) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Anne is red.
("Anne" "is" "red" "+")
triple3
((triple1) -> (rule4 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
((((triple4) -> (rule2 % int2))) -> (rule4 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
((((((triple5 triple2) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
Anne is rough.
("Anne" "is" "rough" "+")
triple4
((triple1 triple3) -> (rule5 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
((triple5 triple2) -> (rule3 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
((triple1 ((triple1) -> (rule4 % int2))) -> (rule5 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
((triple5 ((triple3) -> (rule6 % int2))) -> (rule3 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
((triple5 ((((triple1) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Anne is smart.
("Anne" "is" "smart" "+")
triple5
((triple4) -> (rule1 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
((((triple1 triple3) -> (rule5 % int2))) -> (rule1 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
((((triple1 ((triple1) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Anne is white.
("Anne" "is" "white" "+")
triple6
Anne is young.
("Anne" "is" "young" "+")
triple7
Charlie is rough.
("Charlie" "is" "rough" "+")
triple8
Charlie is white.
("Charlie" "is" "white" "+")
triple9
Charlie is young.
("Charlie" "is" "young" "+")
triple10
Charlie is cold.
("Charlie" "is" "cold" "+")
((triple8) -> (rule2 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
((triple8) -> (rule1 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
((((triple8) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
((((((triple8) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3