Anne is cold. Anne is green. Anne is nice. Anne is quiet. Anne is rough. Fiona is cold. Fiona is nice. Fiona is quiet. Fiona is rough. Fiona is young. All cold, nice people are green. If Fiona is furry and Fiona is quiet then Fiona is young. If Fiona is quiet and Fiona is nice then Fiona is green. Nice people are green. If Fiona is furry and Fiona is nice then Fiona is rough. If someone is quiet then they are rough. If someone is furry then they are green. Quiet people are nice.
Anne is cold.
("Anne" "is" "cold" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Fiona is young.
("Fiona" "is" "young" "+")
All cold, nice people are green.
((("someone" "is" "cold" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "green" "+"))
If Fiona is furry and Fiona is quiet then Fiona is young.
((("Fiona" "is" "furry" "+") ("Fiona" "is" "quiet" "+")) -> ("Fiona" "is" "young" "+"))
If Fiona is quiet and Fiona is nice then Fiona is green.
((("Fiona" "is" "quiet" "+") ("Fiona" "is" "nice" "+")) -> ("Fiona" "is" "green" "+"))
Nice people are green.
((("someone" "is" "nice" "+")) -> ("someone" "is" "green" "+"))
If Fiona is furry and Fiona is nice then Fiona is rough.
((("Fiona" "is" "furry" "+") ("Fiona" "is" "nice" "+")) -> ("Fiona" "is" "rough" "+"))
If someone is quiet then they are rough.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "rough" "+"))
If someone is furry then they are green.
((("someone" "is" "furry" "+")) -> ("someone" "is" "green" "+"))
Quiet people are nice.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "nice" "+"))
Fiona is nice.
True
1
proof
[(triple7 OR ((triple8) -> rule8))]
("Fiona" "is" "nice" "+")
triple7
((triple8) -> (rule8 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is not nice.
False
1
inv-proof
[(triple7 OR ((triple8) -> rule8))]
("Fiona" "is" "nice" "-")
triple7
((triple8) -> (rule8 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is green.
True
2
proof
[(((triple7) -> rule4) OR ((triple6 triple7) -> rule1) OR ((triple8 triple7) -> rule3) OR ((((triple8) -> rule8)) -> rule4) OR ((triple6 ((triple8) -> rule8)) -> rule1) OR ((triple8 ((triple8) -> rule8)) -> rule3))]
("Fiona" "is" "green" "+")
((triple7) -> (rule4 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
((triple6 triple7) -> (rule1 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
((triple8 triple7) -> (rule3 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
((((triple8) -> (rule8 % int2))) -> (rule4 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
((triple6 ((triple8) -> (rule8 % int2))) -> (rule1 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
((triple8 ((triple8) -> (rule8 % int2))) -> (rule3 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is not green.
False
2
inv-proof
[(((triple7) -> rule4) OR ((triple6 triple7) -> rule1) OR ((triple8 triple7) -> rule3) OR ((((triple8) -> rule8)) -> rule4) OR ((triple6 ((triple8) -> rule8)) -> rule1) OR ((triple8 ((triple8) -> rule8)) -> rule3))]
("Fiona" "is" "green" "-")
((triple7) -> (rule4 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
((triple6 triple7) -> (rule1 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
((triple8 triple7) -> (rule3 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
((((triple8) -> (rule8 % int2))) -> (rule4 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
((triple6 ((triple8) -> (rule8 % int2))) -> (rule1 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
((triple8 ((triple8) -> (rule8 % int2))) -> (rule3 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is not furry.
Unknown
inv-random
[@0: Fiona is furry.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "furry" "-")
Anne is furry.
Unknown
random
[@0: Anne is furry.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "furry" "+")
@0: Anne is cold.[(triple1)] Anne is green.[(triple2 OR ((triple3) -> rule4) OR ((triple1 triple3) -> rule1) OR ((((triple4) -> rule8)) -> rule4) OR ((triple1 ((triple4) -> rule8)) -> rule1))] Anne is nice.[(triple3 OR ((triple4) -> rule8))] Anne is quiet.[(triple4)] Anne is rough.[(triple5 OR ((triple4) -> rule6))] Fiona is cold.[(triple6)] Fiona is nice.[(triple7 OR ((triple8) -> rule8))] Fiona is quiet.[(triple8)] Fiona is rough.[(triple9 OR ((triple8) -> rule6))] Fiona is young.[(triple10)] @1: Fiona is green.[(((triple7) -> rule4) OR ((triple6 triple7) -> rule1) OR ((triple8 triple7) -> rule3) OR ((((triple8) -> rule8)) -> rule4) OR ((triple6 ((triple8) -> rule8)) -> rule1) OR ((triple8 ((triple8) -> rule8)) -> rule3))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Anne is green.
("Anne" "is" "green" "+")
triple2
((triple3) -> (rule4 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
((triple1 triple3) -> (rule1 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
((((triple4) -> (rule8 % int2))) -> (rule4 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
((triple1 ((triple4) -> (rule8 % int2))) -> (rule1 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
triple3
((triple4) -> (rule8 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
triple4
Anne is rough.
("Anne" "is" "rough" "+")
triple5
((triple4) -> (rule6 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
triple6
Fiona is nice.
("Fiona" "is" "nice" "+")
triple7
((triple8) -> (rule8 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple8
Fiona is rough.
("Fiona" "is" "rough" "+")
triple9
((triple8) -> (rule6 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
triple10
Fiona is green.
("Fiona" "is" "green" "+")
((triple7) -> (rule4 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
((triple6 triple7) -> (rule1 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
((triple8 triple7) -> (rule3 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
((((triple8) -> (rule8 % int2))) -> (rule4 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
((triple6 ((triple8) -> (rule8 % int2))) -> (rule1 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
((triple8 ((triple8) -> (rule8 % int2))) -> (rule3 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2