Anne is green. Anne is nice. Anne is red. Anne is rough. Charlie is cold. Charlie is green. Charlie is white. All cold things are green. If something is blue and not white then it is not green. Nice things are green. All nice things are cold. Rough things are blue. If something is green then it is nice. Red things are rough. Green, white things are red.
Anne is green.
("Anne" "is" "green" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is white.
("Charlie" "is" "white" "+")
All cold things are green.
((("something" "is" "cold" "+")) -> ("something" "is" "green" "+"))
If something is blue and not white then it is not green.
((("something" "is" "blue" "+") ("something" "is" "white" "~")) -> ("something" "is" "green" "-"))
Nice things are green.
((("something" "is" "nice" "+")) -> ("something" "is" "green" "+"))
All nice things are cold.
((("something" "is" "nice" "+")) -> ("something" "is" "cold" "+"))
Rough things are blue.
((("something" "is" "rough" "+")) -> ("something" "is" "blue" "+"))
If something is green then it is nice.
((("something" "is" "green" "+")) -> ("something" "is" "nice" "+"))
Red things are rough.
((("something" "is" "red" "+")) -> ("something" "is" "rough" "+"))
Green, white things are red.
((("something" "is" "green" "+") ("something" "is" "white" "+")) -> ("something" "is" "red" "+"))
Anne is red.
True
1
proof
[(triple3)]
("Anne" "is" "red" "+")
triple3
Anne is not nice.
False
1
inv-proof
[(triple2 OR ((triple1) -> rule6))]
("Anne" "is" "nice" "-")
triple2
((triple1) -> (rule6 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is blue.
True
2
proof
[(((triple4) -> rule5) OR ((((triple3) -> rule7)) -> rule5))]
("Anne" "is" "blue" "+")
((triple4) -> (rule5 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
((((triple3) -> (rule7 % int2))) -> (rule5 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is not blue.
False
2
inv-proof
[(((triple4) -> rule5) OR ((((triple3) -> rule7)) -> rule5))]
("Anne" "is" "blue" "-")
((triple4) -> (rule5 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
((((triple3) -> (rule7 % int2))) -> (rule5 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
@0: Anne is green.[(triple1 OR ((triple2) -> rule3) OR ((((triple2) -> rule4)) -> rule1))] Anne is nice.[(triple2 OR ((triple1) -> rule6))] Anne is red.[(triple3)] Anne is rough.[(triple4 OR ((triple3) -> rule7))] Charlie is cold.[(triple5 OR ((((triple6) -> rule6)) -> rule4))] Charlie is green.[(triple6 OR ((triple5) -> rule1))] Charlie is white.[(triple7)] @1: Anne is blue.[(((triple4) -> rule5) OR ((((triple3) -> rule7)) -> rule5))] Anne is cold.[(((triple2) -> rule4) OR ((((triple1) -> rule6)) -> rule4))] Charlie is nice.[(((triple6) -> rule6) OR ((((triple5) -> rule1)) -> rule6))] Charlie is red.[(((triple6 triple7) -> rule8) OR ((((triple5) -> rule1) triple7) -> rule8))] @2: Charlie is rough.[(((((triple6 triple7) -> rule8)) -> rule7) OR ((((((triple5) -> rule1) triple7) -> rule8)) -> rule7))] @3: Charlie is blue.[(((((((triple6 triple7) -> rule8)) -> rule7)) -> rule5) OR ((((((((triple5) -> rule1) triple7) -> rule8)) -> rule7)) -> rule5))]
Anne is green.
("Anne" "is" "green" "+")
triple1
((triple2) -> (rule3 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
((((triple2) -> (rule4 % int2))) -> (rule1 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
triple2
((triple1) -> (rule6 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
triple3
Anne is rough.
("Anne" "is" "rough" "+")
triple4
((triple3) -> (rule7 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
triple5
((((triple6) -> (rule6 % int2))) -> (rule4 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
triple6
((triple5) -> (rule1 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
triple7
Anne is blue.
("Anne" "is" "blue" "+")
((triple4) -> (rule5 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
((((triple3) -> (rule7 % int2))) -> (rule5 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
((triple2) -> (rule4 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
((((triple1) -> (rule6 % int2))) -> (rule4 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
((triple6) -> (rule6 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
((((triple5) -> (rule1 % int2))) -> (rule6 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
((triple6 triple7) -> (rule8 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
((((triple5) -> (rule1 % int2)) triple7) -> (rule8 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
((((triple6 triple7) -> (rule8 % int2))) -> (rule7 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
((((((triple5) -> (rule1 % int3)) triple7) -> (rule8 % int2))) -> (rule7 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
Charlie is blue.
("Charlie" "is" "blue" "+")
((((((triple6 triple7) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
((((((((triple5) -> (rule1 % int4)) triple7) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
Charlie is green.
("Charlie" "is" "green" "+")
int4