Anne is furry. Anne is quiet. Anne is red. Anne is rough. Dave is furry. Dave is green. Dave is quiet. Fiona is big. Fiona is quiet. Fiona is rough. If someone is quiet and green then they are rough. All blue people are quiet. If someone is big then they are blue. Rough, green people are blue. Big, blue people are green. Green people are furry. If someone is furry and blue then they are rough. Furry people are red.
Anne is furry.
("Anne" "is" "furry" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
If someone is quiet and green then they are rough.
((("someone" "is" "quiet" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "rough" "+"))
All blue people are quiet.
((("someone" "is" "blue" "+")) -> ("someone" "is" "quiet" "+"))
If someone is big then they are blue.
((("someone" "is" "big" "+")) -> ("someone" "is" "blue" "+"))
Rough, green people are blue.
((("someone" "is" "rough" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "blue" "+"))
Big, blue people are green.
((("someone" "is" "big" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "green" "+"))
Green people are furry.
((("someone" "is" "green" "+")) -> ("someone" "is" "furry" "+"))
If someone is furry and blue then they are rough.
((("someone" "is" "furry" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "rough" "+"))
Furry people are red.
((("someone" "is" "furry" "+")) -> ("someone" "is" "red" "+"))
Fiona is quiet.
True
1
proof
[(triple9 OR ((((triple8) -> rule3)) -> rule2))]
("Fiona" "is" "quiet" "+")
triple9
((((triple8) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Dave is not green.
False
1
inv-proof
[(triple6)]
("Dave" "is" "green" "-")
triple6
Dave is rough.
True
3
proof
[(((triple7 triple6) -> rule1))]
("Dave" "is" "rough" "+")
((triple7 triple6) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is not red.
False
2
inv-proof
[(((triple5) -> rule8) OR ((((triple6) -> rule6)) -> rule8))]
("Dave" "is" "red" "-")
((triple5) -> (rule8 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
((((triple6) -> (rule6 % int2))) -> (rule8 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is blue.
True
5
proof
[(((((triple7 triple6) -> rule1) triple6) -> rule4))]
("Dave" "is" "blue" "+")
((((triple7 triple6) -> (rule1 % int2)) triple6) -> (rule4 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is not blue.
False
5
inv-proof
[(((((triple7 triple6) -> rule1) triple6) -> rule4))]
("Dave" "is" "blue" "-")
((((triple7 triple6) -> (rule1 % int2)) triple6) -> (rule4 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Anne is not green.
Unknown
inv-rconc
[@1: Anne is green.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Anne" "is" "green" "-")
Anne is blue.
Unknown
rconc
[@2: Anne is blue.[CWA. Example of deepest failure = (rule4 <- rule5 <- FAIL)]]
("Anne" "is" "blue" "+")
Dave is not big.
Unknown
inv-random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "-")
Anne is big.
Unknown
random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "+")
@0: Anne is furry.[(triple1)] Anne is quiet.[(triple2)] Anne is red.[(triple3 OR ((triple1) -> rule8))] Anne is rough.[(triple4)] Dave is furry.[(triple5 OR ((triple6) -> rule6))] Dave is green.[(triple6)] Dave is quiet.[(triple7)] Fiona is big.[(triple8)] Fiona is quiet.[(triple9 OR ((((triple8) -> rule3)) -> rule2))] Fiona is rough.[(triple10 OR ((triple9 ((triple8 ((triple8) -> rule3)) -> rule5)) -> rule1) OR ((((((triple8) -> rule3)) -> rule2) ((triple8 ((triple8) -> rule3)) -> rule5)) -> rule1) OR ((((((triple8 ((triple8) -> rule3)) -> rule5)) -> rule6) ((triple8) -> rule3)) -> rule7))] @1: Dave is red.[(((triple5) -> rule8) OR ((((triple6) -> rule6)) -> rule8))] Dave is rough.[(((triple7 triple6) -> rule1))] Fiona is blue.[(((triple8) -> rule3))] @2: Dave is blue.[(((((triple7 triple6) -> rule1) triple6) -> rule4))] Fiona is green.[(((triple8 ((triple8) -> rule3)) -> rule5))] @3: Fiona is furry.[(((((triple8 ((triple8) -> rule3)) -> rule5)) -> rule6))] @4: Fiona is red.[(((((((triple8 ((triple8) -> rule3)) -> rule5)) -> rule6)) -> rule8))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Anne is quiet.
("Anne" "is" "quiet" "+")
triple2
Anne is red.
("Anne" "is" "red" "+")
triple3
((triple1) -> (rule8 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
triple4
Dave is furry.
("Dave" "is" "furry" "+")
triple5
((triple6) -> (rule6 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
triple6
Dave is quiet.
("Dave" "is" "quiet" "+")
triple7
Fiona is big.
("Fiona" "is" "big" "+")
triple8
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple9
((((triple8) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
triple10
((triple9 ((triple8 ((triple8) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
int3
((((((triple8) -> (rule3 % int4))) -> (rule2 % int3)) ((triple8 ((triple8) -> (rule3 % int4))) -> (rule5 % int2))) -> (rule1 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int3
Fiona is blue.
("Fiona" "is" "blue" "+")
int4
((((((triple8 ((triple8) -> (rule3 % int4))) -> (rule5 % int3))) -> (rule6 % int2)) ((triple8) -> (rule3 % int4))) -> (rule7 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
int3
Fiona is blue.
("Fiona" "is" "blue" "+")
int4
Dave is red.
("Dave" "is" "red" "+")
((triple5) -> (rule8 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
((((triple6) -> (rule6 % int2))) -> (rule8 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
((triple7 triple6) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
((triple8) -> (rule3 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
((((triple7 triple6) -> (rule1 % int2)) triple6) -> (rule4 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
((triple8 ((triple8) -> (rule3 % int2))) -> (rule5 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is furry.
("Fiona" "is" "furry" "+")
((((triple8 ((triple8) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
int3
Fiona is red.
("Fiona" "is" "red" "+")
((((((triple8 ((triple8) -> (rule3 % int4))) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
int3
Fiona is blue.
("Fiona" "is" "blue" "+")
int4