Anne is not big. Anne is blue. Anne is cold. Anne is nice. Anne is rough. Anne is not round. Anne is white. Nice things are white. Round, nice things are not white. If something is nice then it is white. If Anne is nice then Anne is blue. If Anne is round and Anne is nice then Anne is big. All rough things are not big. If Anne is round and Anne is rough then Anne is cold. If Anne is big and Anne is blue then Anne is rough.
Anne is not big.
("Anne" "is" "big" "-")
Anne is blue.
("Anne" "is" "blue" "+")
Anne is cold.
("Anne" "is" "cold" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is not round.
("Anne" "is" "round" "-")
Anne is white.
("Anne" "is" "white" "+")
Nice things are white.
((("something" "is" "nice" "+")) -> ("something" "is" "white" "+"))
Round, nice things are not white.
((("something" "is" "round" "+") ("something" "is" "nice" "+")) -> ("something" "is" "white" "-"))
If something is nice then it is white.
((("something" "is" "nice" "+")) -> ("something" "is" "white" "+"))
If Anne is nice then Anne is blue.
((("Anne" "is" "nice" "+")) -> ("Anne" "is" "blue" "+"))
If Anne is round and Anne is nice then Anne is big.
((("Anne" "is" "round" "+") ("Anne" "is" "nice" "+")) -> ("Anne" "is" "big" "+"))
All rough things are not big.
((("something" "is" "rough" "+")) -> ("something" "is" "big" "-"))
If Anne is round and Anne is rough then Anne is cold.
((("Anne" "is" "round" "+") ("Anne" "is" "rough" "+")) -> ("Anne" "is" "cold" "+"))
If Anne is big and Anne is blue then Anne is rough.
((("Anne" "is" "big" "+") ("Anne" "is" "blue" "+")) -> ("Anne" "is" "rough" "+"))
Anne is rough.
True
1
proof
[(triple5)]
("Anne" "is" "rough" "+")
triple5
Anne is not white.
False
1
inv-proof
[(triple7 OR ((triple4) -> rule1) OR ((triple4) -> rule3))]
("Anne" "is" "white" "-")
triple7
((triple4) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
((triple4) -> (rule3 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
@0: Anne is blue.[(triple2 OR ((triple4) -> rule4))] Anne is cold.[(triple3)] Anne is nice.[(triple4)] Anne is not big.[(triple1 OR ((triple5) -> rule6))] Anne is not round.[(triple6)] Anne is rough.[(triple5)] Anne is white.[(triple7 OR ((triple4) -> rule1) OR ((triple4) -> rule3))]
Anne is blue.
("Anne" "is" "blue" "+")
triple2
((triple4) -> (rule4 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
triple3
Anne is nice.
("Anne" "is" "nice" "+")
triple4
Anne is not big.
("Anne" "is" "big" "-")
triple1
((triple5) -> (rule6 % int1))
Anne is not big.
("Anne" "is" "big" "-")
int1
Anne is not round.
("Anne" "is" "round" "-")
triple6
Anne is rough.
("Anne" "is" "rough" "+")
triple5
Anne is white.
("Anne" "is" "white" "+")
triple7
((triple4) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
((triple4) -> (rule3 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1