Anne is blue. Anne is cold. Anne is not green. Bob is blue. Bob is cold. Bob is quiet. Fiona is not big. Big things are quiet. If Bob is quiet then Bob is not red. If something is big then it is cold. Big, cold things are green. All quiet things are big. If Anne is kind then Anne is red. If something is big and not cold then it is not red. If something is big and not green then it is kind.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is cold.
("Anne" "is" "cold" "+")
Anne is not green.
("Anne" "is" "green" "-")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Fiona is not big.
("Fiona" "is" "big" "-")
Big things are quiet.
((("something" "is" "big" "+")) -> ("something" "is" "quiet" "+"))
If Bob is quiet then Bob is not red.
((("Bob" "is" "quiet" "+")) -> ("Bob" "is" "red" "-"))
If something is big then it is cold.
((("something" "is" "big" "+")) -> ("something" "is" "cold" "+"))
Big, cold things are green.
((("something" "is" "big" "+") ("something" "is" "cold" "+")) -> ("something" "is" "green" "+"))
All quiet things are big.
((("something" "is" "quiet" "+")) -> ("something" "is" "big" "+"))
If Anne is kind then Anne is red.
((("Anne" "is" "kind" "+")) -> ("Anne" "is" "red" "+"))
If something is big and not cold then it is not red.
((("something" "is" "big" "+") ("something" "is" "cold" "~")) -> ("something" "is" "red" "-"))
If something is big and not green then it is kind.
((("something" "is" "big" "+") ("something" "is" "green" "~")) -> ("something" "is" "kind" "+"))
Anne is cold.
True
1
proof
[(triple2)]
("Anne" "is" "cold" "+")
triple2
Anne is green.
False
1
inv-proof
[(triple3)]
("Anne" "is" "green" "+")
triple3
Fiona is not green.
Unknown
inv-rconc
[@1: Fiona is green.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Fiona" "is" "green" "-")
Fiona is red.
Unknown
random
[@0: Fiona is red.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "red" "+")
@0: Anne is blue.[(triple1)] Anne is cold.[(triple2)] Anne is not green.[(triple3)] Bob is blue.[(triple4)] Bob is cold.[(triple5 OR ((((triple6) -> rule5)) -> rule3))] Bob is quiet.[(triple6)] Fiona is not big.[(triple7)] @1: Bob is big.[(((triple6) -> rule5))] Bob is not red.[(((triple6) -> rule2))] @2: Bob is green.[(((((triple6) -> rule5) triple5) -> rule4) OR ((((triple6) -> rule5) ((((triple6) -> rule5)) -> rule3)) -> rule4))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is cold.
("Anne" "is" "cold" "+")
triple2
Anne is not green.
("Anne" "is" "green" "-")
triple3
Bob is blue.
("Bob" "is" "blue" "+")
triple4
Bob is cold.
("Bob" "is" "cold" "+")
triple5
((((triple6) -> (rule5 % int2))) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
triple6
Fiona is not big.
("Fiona" "is" "big" "-")
triple7
Bob is big.
("Bob" "is" "big" "+")
((triple6) -> (rule5 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is not red.
("Bob" "is" "red" "-")
((triple6) -> (rule2 % int1))
Bob is not red.
("Bob" "is" "red" "-")
int1
Bob is green.
("Bob" "is" "green" "+")
((((triple6) -> (rule5 % int2)) triple5) -> (rule4 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
((((triple6) -> (rule5 % int3)) ((((triple6) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3