Anne is quiet. Anne is round. Dave is round. Dave is white. Fiona is blue. Fiona is furry. Fiona is round. If someone is young then they are round. If someone is round and blue then they are cold. All furry people are blue. If Anne is round then Anne is furry. All cold, round people are quiet. If someone is furry then they are round.
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is round.
("Anne" "is" "round" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is white.
("Dave" "is" "white" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is round.
("Fiona" "is" "round" "+")
If someone is young then they are round.
((("someone" "is" "young" "+")) -> ("someone" "is" "round" "+"))
If someone is round and blue then they are cold.
((("someone" "is" "round" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "cold" "+"))
All furry people are blue.
((("someone" "is" "furry" "+")) -> ("someone" "is" "blue" "+"))
If Anne is round then Anne is furry.
((("Anne" "is" "round" "+")) -> ("Anne" "is" "furry" "+"))
All cold, round people are quiet.
((("someone" "is" "cold" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "quiet" "+"))
If someone is furry then they are round.
((("someone" "is" "furry" "+")) -> ("someone" "is" "round" "+"))
Anne is quiet.
True
1
proof
[(triple1 OR ((((triple2 ((((triple2) -> rule4)) -> rule3)) -> rule2) triple2) -> rule5))]
("Anne" "is" "quiet" "+")
triple1
((((triple2 ((((triple2) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule2 % int2)) triple2) -> (rule5 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
Anne is furry.
("Anne" "is" "furry" "+")
int4
Fiona is not furry.
False
1
inv-proof
[(triple6)]
("Fiona" "is" "furry" "-")
triple6
Anne is furry.
True
2
proof
[(((triple2) -> rule4))]
("Anne" "is" "furry" "+")
((triple2) -> (rule4 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is not furry.
False
2
inv-proof
[(((triple2) -> rule4))]
("Anne" "is" "furry" "-")
((triple2) -> (rule4 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Fiona is quiet.
True
5
proof
[(((((triple7 triple5) -> rule2) triple7) -> rule5) OR ((((triple7 triple5) -> rule2) ((triple6) -> rule6)) -> rule5) OR ((((triple7 ((triple6) -> rule3)) -> rule2) triple7) -> rule5) OR ((((((triple6) -> rule6) triple5) -> rule2) triple7) -> rule5) OR ((((triple7 ((triple6) -> rule3)) -> rule2) ((triple6) -> rule6)) -> rule5) OR ((((((triple6) -> rule6) triple5) -> rule2) ((triple6) -> rule6)) -> rule5) OR ((((((triple6) -> rule6) ((triple6) -> rule3)) -> rule2) triple7) -> rule5) OR ((((((triple6) -> rule6) ((triple6) -> rule3)) -> rule2) ((triple6) -> rule6)) -> rule5))]
("Fiona" "is" "quiet" "+")
((((triple7 triple5) -> (rule2 % int2)) triple7) -> (rule5 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
((((triple7 triple5) -> (rule2 % int3)) ((triple6) -> (rule6 % int2))) -> (rule5 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
int3
((((triple7 ((triple6) -> (rule3 % int3))) -> (rule2 % int2)) triple7) -> (rule5 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
int3
((((((triple6) -> (rule6 % int3)) triple5) -> (rule2 % int2)) triple7) -> (rule5 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
int3
((((triple7 ((triple6) -> (rule3 % int4))) -> (rule2 % int3)) ((triple6) -> (rule6 % int2))) -> (rule5 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
int3
Fiona is blue.
("Fiona" "is" "blue" "+")
int4
((((((triple6) -> (rule6 % int3)) triple5) -> (rule2 % int2)) ((triple6) -> (rule6 % int3))) -> (rule5 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
int3
((((((triple6) -> (rule6 % int4)) ((triple6) -> (rule3 % int3))) -> (rule2 % int2)) triple7) -> (rule5 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
int3
Fiona is round.
("Fiona" "is" "round" "+")
int4
((((((triple6) -> (rule6 % int4)) ((triple6) -> (rule3 % int3))) -> (rule2 % int2)) ((triple6) -> (rule6 % int4))) -> (rule5 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
int3
Fiona is round.
("Fiona" "is" "round" "+")
int4
Anne is not blue.
False
3
inv-proof
[(((((triple2) -> rule4)) -> rule3))]
("Anne" "is" "blue" "-")
((((triple2) -> (rule4 % int2))) -> (rule3 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Dave is not cold.
Unknown
inv-rconc
[@2: Dave is cold.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("Dave" "is" "cold" "-")
Dave is blue.
Unknown
rconc
[@1: Dave is blue.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "blue" "+")
Dave is not quiet.
Unknown
inv-rconc
[@3: Dave is quiet.[CWA. Example of deepest failure = (rule5 <- rule2 <- rule3 <- FAIL)]]
("Dave" "is" "quiet" "-")
Fiona is young.
Unknown
random
[@0: Fiona is young.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "young" "+")
Anne is not white.
Unknown
inv-random
[@0: Anne is white.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "white" "-")
Dave is young.
Unknown
random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "+")
@0: Anne is quiet.[(triple1 OR ((((triple2 ((((triple2) -> rule4)) -> rule3)) -> rule2) triple2) -> rule5))] Anne is round.[(triple2)] Dave is round.[(triple3)] Dave is white.[(triple4)] Fiona is blue.[(triple5 OR ((triple6) -> rule3))] Fiona is furry.[(triple6)] Fiona is round.[(triple7 OR ((triple6) -> rule6))] @1: Anne is furry.[(((triple2) -> rule4))] Fiona is cold.[(((triple7 triple5) -> rule2) OR ((triple7 ((triple6) -> rule3)) -> rule2) OR ((((triple6) -> rule6) triple5) -> rule2) OR ((((triple6) -> rule6) ((triple6) -> rule3)) -> rule2))] @2: Anne is blue.[(((((triple2) -> rule4)) -> rule3))] Fiona is quiet.[(((((triple7 triple5) -> rule2) triple7) -> rule5) OR ((((triple7 triple5) -> rule2) ((triple6) -> rule6)) -> rule5) OR ((((triple7 ((triple6) -> rule3)) -> rule2) triple7) -> rule5) OR ((((((triple6) -> rule6) triple5) -> rule2) triple7) -> rule5) OR ((((triple7 ((triple6) -> rule3)) -> rule2) ((triple6) -> rule6)) -> rule5) OR ((((((triple6) -> rule6) triple5) -> rule2) ((triple6) -> rule6)) -> rule5) OR ((((((triple6) -> rule6) ((triple6) -> rule3)) -> rule2) triple7) -> rule5) OR ((((((triple6) -> rule6) ((triple6) -> rule3)) -> rule2) ((triple6) -> rule6)) -> rule5))] @3: Anne is cold.[(((triple2 ((((triple2) -> rule4)) -> rule3)) -> rule2))]
Anne is quiet.
("Anne" "is" "quiet" "+")
triple1
((((triple2 ((((triple2) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule2 % int2)) triple2) -> (rule5 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
Anne is furry.
("Anne" "is" "furry" "+")
int4
Anne is round.
("Anne" "is" "round" "+")
triple2
Dave is round.
("Dave" "is" "round" "+")
triple3
Dave is white.
("Dave" "is" "white" "+")
triple4
Fiona is blue.
("Fiona" "is" "blue" "+")
triple5
((triple6) -> (rule3 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
triple6
Fiona is round.
("Fiona" "is" "round" "+")
triple7
((triple6) -> (rule6 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
((triple2) -> (rule4 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
((triple7 triple5) -> (rule2 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
((triple7 ((triple6) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
((((triple6) -> (rule6 % int2)) triple5) -> (rule2 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
((((triple6) -> (rule6 % int3)) ((triple6) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
int3
Anne is blue.
("Anne" "is" "blue" "+")
((((triple2) -> (rule4 % int2))) -> (rule3 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
((((triple7 triple5) -> (rule2 % int2)) triple7) -> (rule5 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
((((triple7 triple5) -> (rule2 % int3)) ((triple6) -> (rule6 % int2))) -> (rule5 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
int3
((((triple7 ((triple6) -> (rule3 % int3))) -> (rule2 % int2)) triple7) -> (rule5 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
int3
((((((triple6) -> (rule6 % int3)) triple5) -> (rule2 % int2)) triple7) -> (rule5 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
int3
((((triple7 ((triple6) -> (rule3 % int4))) -> (rule2 % int3)) ((triple6) -> (rule6 % int2))) -> (rule5 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
int3
Fiona is blue.
("Fiona" "is" "blue" "+")
int4
((((((triple6) -> (rule6 % int3)) triple5) -> (rule2 % int2)) ((triple6) -> (rule6 % int3))) -> (rule5 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
int3
((((((triple6) -> (rule6 % int4)) ((triple6) -> (rule3 % int3))) -> (rule2 % int2)) triple7) -> (rule5 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
int3
Fiona is round.
("Fiona" "is" "round" "+")
int4
((((((triple6) -> (rule6 % int4)) ((triple6) -> (rule3 % int3))) -> (rule2 % int2)) ((triple6) -> (rule6 % int4))) -> (rule5 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
int3
Fiona is round.
("Fiona" "is" "round" "+")
int4
Anne is cold.
("Anne" "is" "cold" "+")
((triple2 ((((triple2) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3