Anne is cold. Anne is nice. Anne is quiet. Anne is white. Charlie is quiet. Dave is furry. Fiona is cold. If something is furry then it is quiet. All blue things are white. Nice, cold things are furry. If something is white and furry then it is rough. Blue, quiet things are furry. Nice, quiet things are white.
Anne is cold.
("Anne" "is" "cold" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is white.
("Anne" "is" "white" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
If something is furry then it is quiet.
((("something" "is" "furry" "+")) -> ("something" "is" "quiet" "+"))
All blue things are white.
((("something" "is" "blue" "+")) -> ("something" "is" "white" "+"))
Nice, cold things are furry.
((("something" "is" "nice" "+") ("something" "is" "cold" "+")) -> ("something" "is" "furry" "+"))
If something is white and furry then it is rough.
((("something" "is" "white" "+") ("something" "is" "furry" "+")) -> ("something" "is" "rough" "+"))
Blue, quiet things are furry.
((("something" "is" "blue" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "furry" "+"))
Nice, quiet things are white.
((("something" "is" "nice" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "white" "+"))
Anne is cold.
True
1
proof
[(triple1)]
("Anne" "is" "cold" "+")
triple1
Anne is not quiet.
False
1
inv-proof
[(triple3 OR ((((triple2 triple1) -> rule3)) -> rule1))]
("Anne" "is" "quiet" "-")
triple3
((((triple2 triple1) -> (rule3 % int2))) -> (rule1 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Charlie is not rough.
Unknown
inv-rconc
[@2: Charlie is rough.[CWA. Example of deepest failure = (rule4 <- rule2 <- FAIL)]]
("Charlie" "is" "rough" "-")
Fiona is nice.
Unknown
random
[@0: Fiona is nice.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "nice" "+")
@0: Anne is cold.[(triple1)] Anne is nice.[(triple2)] Anne is quiet.[(triple3 OR ((((triple2 triple1) -> rule3)) -> rule1))] Anne is white.[(triple4 OR ((triple2 triple3) -> rule6) OR ((triple2 ((((triple2 triple1) -> rule3)) -> rule1)) -> rule6))] Charlie is quiet.[(triple5)] Dave is furry.[(triple6)] Fiona is cold.[(triple7)] @1: Anne is furry.[(((triple2 triple1) -> rule3))] Dave is quiet.[(((triple6) -> rule1))] @2: Anne is rough.[(((triple4 ((triple2 triple1) -> rule3)) -> rule4) OR ((((triple2 triple3) -> rule6) ((triple2 triple1) -> rule3)) -> rule4) OR ((((triple2 ((((triple2 triple1) -> rule3)) -> rule1)) -> rule6) ((triple2 triple1) -> rule3)) -> rule4))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Anne is nice.
("Anne" "is" "nice" "+")
triple2
Anne is quiet.
("Anne" "is" "quiet" "+")
triple3
((((triple2 triple1) -> (rule3 % int2))) -> (rule1 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
triple4
((triple2 triple3) -> (rule6 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
((triple2 ((((triple2 triple1) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple5
Dave is furry.
("Dave" "is" "furry" "+")
triple6
Fiona is cold.
("Fiona" "is" "cold" "+")
triple7
Anne is furry.
("Anne" "is" "furry" "+")
((triple2 triple1) -> (rule3 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
((triple6) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
((triple4 ((triple2 triple1) -> (rule3 % int2))) -> (rule4 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
((((triple2 triple3) -> (rule6 % int3)) ((triple2 triple1) -> (rule3 % int2))) -> (rule4 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
((((triple2 ((((triple2 triple1) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule6 % int2)) ((triple2 triple1) -> (rule3 % int4))) -> (rule4 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
Anne is furry.
("Anne" "is" "furry" "+")
int4