Anne is blue. Anne is kind. Anne is rough. Anne is young. Erin is cold. Erin is kind. Erin is rough. Erin is young. Fiona is quiet. Fiona is rough. If something is quiet then it is young. Big things are kind. All quiet things are blue. If something is rough then it is big. If something is quiet then it is blue. If Erin is cold and Erin is big then Erin is quiet.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is young.
("Anne" "is" "young" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is young.
("Erin" "is" "young" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
If something is quiet then it is young.
((("something" "is" "quiet" "+")) -> ("something" "is" "young" "+"))
Big things are kind.
((("something" "is" "big" "+")) -> ("something" "is" "kind" "+"))
All quiet things are blue.
((("something" "is" "quiet" "+")) -> ("something" "is" "blue" "+"))
If something is rough then it is big.
((("something" "is" "rough" "+")) -> ("something" "is" "big" "+"))
If something is quiet then it is blue.
((("something" "is" "quiet" "+")) -> ("something" "is" "blue" "+"))
If Erin is cold and Erin is big then Erin is quiet.
((("Erin" "is" "cold" "+") ("Erin" "is" "big" "+")) -> ("Erin" "is" "quiet" "+"))
Anne is kind.
True
1
proof
[(triple2 OR ((((triple3) -> rule4)) -> rule2))]
("Anne" "is" "kind" "+")
triple2
((((triple3) -> (rule4 % int2))) -> (rule2 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is not kind.
False
1
inv-proof
[(triple2 OR ((((triple3) -> rule4)) -> rule2))]
("Anne" "is" "kind" "-")
triple2
((((triple3) -> (rule4 % int2))) -> (rule2 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is big.
True
2
proof
[(((triple3) -> rule4))]
("Anne" "is" "big" "+")
((triple3) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Fiona is not young.
False
2
inv-proof
[(((triple9) -> rule1))]
("Fiona" "is" "young" "-")
((triple9) -> (rule1 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Erin is quiet.
True
4
proof
[(((triple5 ((triple7) -> rule4)) -> rule6))]
("Erin" "is" "quiet" "+")
((triple5 ((triple7) -> (rule4 % int2))) -> (rule6 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is not quiet.
False
4
inv-proof
[(((triple5 ((triple7) -> rule4)) -> rule6))]
("Erin" "is" "quiet" "-")
((triple5 ((triple7) -> (rule4 % int2))) -> (rule6 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is blue.
True
5
proof
[(((((triple5 ((triple7) -> rule4)) -> rule6)) -> rule3) OR ((((triple5 ((triple7) -> rule4)) -> rule6)) -> rule5))]
("Erin" "is" "blue" "+")
((((triple5 ((triple7) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
((((triple5 ((triple7) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Erin is not blue.
False
5
inv-proof
[(((((triple5 ((triple7) -> rule4)) -> rule6)) -> rule3) OR ((((triple5 ((triple7) -> rule4)) -> rule6)) -> rule5))]
("Erin" "is" "blue" "-")
((((triple5 ((triple7) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
((((triple5 ((triple7) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Anne is not quiet.
Unknown
inv-random
[@0: Anne is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "quiet" "-")
Anne is cold.
Unknown
random
[@0: Anne is cold.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "cold" "+")
@0: Anne is blue.[(triple1)] Anne is kind.[(triple2 OR ((((triple3) -> rule4)) -> rule2))] Anne is rough.[(triple3)] Anne is young.[(triple4)] Erin is cold.[(triple5)] Erin is kind.[(triple6 OR ((((triple7) -> rule4)) -> rule2))] Erin is rough.[(triple7)] Erin is young.[(triple8 OR ((((triple5 ((triple7) -> rule4)) -> rule6)) -> rule1))] Fiona is quiet.[(triple9)] Fiona is rough.[(triple10)] @1: Anne is big.[(((triple3) -> rule4))] Erin is big.[(((triple7) -> rule4))] Fiona is big.[(((triple10) -> rule4))] Fiona is blue.[(((triple9) -> rule3) OR ((triple9) -> rule5))] Fiona is young.[(((triple9) -> rule1))] @2: Erin is quiet.[(((triple5 ((triple7) -> rule4)) -> rule6))] Fiona is kind.[(((((triple10) -> rule4)) -> rule2))] @3: Erin is blue.[(((((triple5 ((triple7) -> rule4)) -> rule6)) -> rule3) OR ((((triple5 ((triple7) -> rule4)) -> rule6)) -> rule5))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is kind.
("Anne" "is" "kind" "+")
triple2
((((triple3) -> (rule4 % int2))) -> (rule2 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
triple3
Anne is young.
("Anne" "is" "young" "+")
triple4
Erin is cold.
("Erin" "is" "cold" "+")
triple5
Erin is kind.
("Erin" "is" "kind" "+")
triple6
((((triple7) -> (rule4 % int2))) -> (rule2 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
triple7
Erin is young.
("Erin" "is" "young" "+")
triple8
((((triple5 ((triple7) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple9
Fiona is rough.
("Fiona" "is" "rough" "+")
triple10
Anne is big.
("Anne" "is" "big" "+")
((triple3) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
((triple7) -> (rule4 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
((triple10) -> (rule4 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
((triple9) -> (rule3 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
((triple9) -> (rule5 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
((triple9) -> (rule1 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
((triple5 ((triple7) -> (rule4 % int2))) -> (rule6 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
((((triple10) -> (rule4 % int2))) -> (rule2 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
((((triple5 ((triple7) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
((((triple5 ((triple7) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3