Anne is kind. Anne is rough. Erin is cold. Erin is red. Erin is rough. Fiona is red. Fiona is rough. If something is red then it is kind. Kind, rough things are young. Green things are rough. Cold things are green. If something is red then it is cold. If something is red then it is rough. If Anne is green then Anne is young. All kind things are green.
Anne is kind.
("Anne" "is" "kind" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
If something is red then it is kind.
((("something" "is" "red" "+")) -> ("something" "is" "kind" "+"))
Kind, rough things are young.
((("something" "is" "kind" "+") ("something" "is" "rough" "+")) -> ("something" "is" "young" "+"))
Green things are rough.
((("something" "is" "green" "+")) -> ("something" "is" "rough" "+"))
Cold things are green.
((("something" "is" "cold" "+")) -> ("something" "is" "green" "+"))
If something is red then it is cold.
((("something" "is" "red" "+")) -> ("something" "is" "cold" "+"))
If something is red then it is rough.
((("something" "is" "red" "+")) -> ("something" "is" "rough" "+"))
If Anne is green then Anne is young.
((("Anne" "is" "green" "+")) -> ("Anne" "is" "young" "+"))
All kind things are green.
((("something" "is" "kind" "+")) -> ("something" "is" "green" "+"))
Fiona is rough.
True
1
proof
[(triple7 OR ((triple6) -> rule6) OR ((((((triple6) -> rule1)) -> rule8)) -> rule3) OR ((((((triple6) -> rule5)) -> rule4)) -> rule3))]
("Fiona" "is" "rough" "+")
triple7
((triple6) -> (rule6 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
((((((triple6) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule3 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
int3
((((((triple6) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
int3
Erin is not rough.
False
1
inv-proof
[(triple5 OR ((triple4) -> rule6) OR ((((triple3) -> rule4)) -> rule3) OR ((((((triple4) -> rule1)) -> rule8)) -> rule3) OR ((((((triple4) -> rule5)) -> rule4)) -> rule3))]
("Erin" "is" "rough" "-")
triple5
((triple4) -> (rule6 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
((((triple3) -> (rule4 % int2))) -> (rule3 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
((((((triple4) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule3 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
((((((triple4) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Erin is kind.
True
2
proof
[(((triple4) -> rule1))]
("Erin" "is" "kind" "+")
((triple4) -> (rule1 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is not kind.
False
2
inv-proof
[(((triple4) -> rule1))]
("Erin" "is" "kind" "-")
((triple4) -> (rule1 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Fiona is young.
True
4
proof
[(((((triple6) -> rule1) triple7) -> rule2) OR ((((triple6) -> rule1) ((triple6) -> rule6)) -> rule2) OR ((((triple6) -> rule1) ((((((triple6) -> rule1)) -> rule8)) -> rule3)) -> rule2) OR ((((triple6) -> rule1) ((((((triple6) -> rule5)) -> rule4)) -> rule3)) -> rule2))]
("Fiona" "is" "young" "+")
((((triple6) -> (rule1 % int2)) triple7) -> (rule2 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
((((triple6) -> (rule1 % int3)) ((triple6) -> (rule6 % int2))) -> (rule2 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
int3
((((triple6) -> (rule1 % int4)) ((((((triple6) -> (rule1 % int4))) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
int3
Fiona is kind.
("Fiona" "is" "kind" "+")
int4
((((triple6) -> (rule1 % int5)) ((((((triple6) -> (rule5 % int4))) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
int3
Fiona is cold.
("Fiona" "is" "cold" "+")
int4
Fiona is kind.
("Fiona" "is" "kind" "+")
int5
Fiona is not green.
False
3
inv-proof
[(((((triple6) -> rule1)) -> rule8) OR ((((triple6) -> rule5)) -> rule4))]
("Fiona" "is" "green" "-")
((((triple6) -> (rule1 % int2))) -> (rule8 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
((((triple6) -> (rule5 % int2))) -> (rule4 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Anne is not cold.
Unknown
inv-rconc
[@1: Anne is cold.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Anne" "is" "cold" "-")
Anne is furry.
Unknown
random
[@0: Anne is furry.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "furry" "+")
Anne is not red.
Unknown
inv-random
[@0: Anne is red.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "red" "-")
Fiona is furry.
Unknown
random
[@0: Fiona is furry.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "furry" "+")
@0: Anne is kind.[(triple1)] Anne is rough.[(triple2 OR ((((triple1) -> rule8)) -> rule3))] Erin is cold.[(triple3 OR ((triple4) -> rule5))] Erin is red.[(triple4)] Erin is rough.[(triple5 OR ((triple4) -> rule6) OR ((((triple3) -> rule4)) -> rule3) OR ((((((triple4) -> rule1)) -> rule8)) -> rule3) OR ((((((triple4) -> rule5)) -> rule4)) -> rule3))] Fiona is red.[(triple6)] Fiona is rough.[(triple7 OR ((triple6) -> rule6) OR ((((((triple6) -> rule1)) -> rule8)) -> rule3) OR ((((((triple6) -> rule5)) -> rule4)) -> rule3))] @1: Anne is green.[(((triple1) -> rule8))] Anne is young.[(((triple1 triple2) -> rule2) OR ((((triple1) -> rule8)) -> rule7) OR ((triple1 ((((triple1) -> rule8)) -> rule3)) -> rule2))] Erin is green.[(((triple3) -> rule4) OR ((((triple4) -> rule1)) -> rule8) OR ((((triple4) -> rule5)) -> rule4))] Erin is kind.[(((triple4) -> rule1))] Fiona is cold.[(((triple6) -> rule5))] Fiona is kind.[(((triple6) -> rule1))] @2: Erin is young.[(((((triple4) -> rule1) triple5) -> rule2) OR ((((triple4) -> rule1) ((triple4) -> rule6)) -> rule2) OR ((((triple4) -> rule1) ((((triple3) -> rule4)) -> rule3)) -> rule2) OR ((((triple4) -> rule1) ((((((triple4) -> rule1)) -> rule8)) -> rule3)) -> rule2) OR ((((triple4) -> rule1) ((((((triple4) -> rule5)) -> rule4)) -> rule3)) -> rule2))] Fiona is green.[(((((triple6) -> rule1)) -> rule8) OR ((((triple6) -> rule5)) -> rule4))] Fiona is young.[(((((triple6) -> rule1) triple7) -> rule2) OR ((((triple6) -> rule1) ((triple6) -> rule6)) -> rule2) OR ((((triple6) -> rule1) ((((((triple6) -> rule1)) -> rule8)) -> rule3)) -> rule2) OR ((((triple6) -> rule1) ((((((triple6) -> rule5)) -> rule4)) -> rule3)) -> rule2))]
Anne is kind.
("Anne" "is" "kind" "+")
triple1
Anne is rough.
("Anne" "is" "rough" "+")
triple2
((((triple1) -> (rule8 % int2))) -> (rule3 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
triple3
((triple4) -> (rule5 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
triple4
Erin is rough.
("Erin" "is" "rough" "+")
triple5
((triple4) -> (rule6 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
((((triple3) -> (rule4 % int2))) -> (rule3 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
((((((triple4) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule3 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
((((((triple4) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Fiona is red.
("Fiona" "is" "red" "+")
triple6
Fiona is rough.
("Fiona" "is" "rough" "+")
triple7
((triple6) -> (rule6 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
((((((triple6) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule3 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
int3
((((((triple6) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
int3
Anne is green.
("Anne" "is" "green" "+")
((triple1) -> (rule8 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
((triple1 triple2) -> (rule2 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
((((triple1) -> (rule8 % int2))) -> (rule7 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
((triple1 ((((triple1) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Erin is green.
("Erin" "is" "green" "+")
((triple3) -> (rule4 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
((((triple4) -> (rule1 % int2))) -> (rule8 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
((((triple4) -> (rule5 % int2))) -> (rule4 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
((triple4) -> (rule1 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
((triple6) -> (rule5 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
((triple6) -> (rule1 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
((((triple4) -> (rule1 % int2)) triple5) -> (rule2 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
((((triple4) -> (rule1 % int3)) ((triple4) -> (rule6 % int2))) -> (rule2 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
((((triple4) -> (rule1 % int4)) ((((triple3) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Erin is kind.
("Erin" "is" "kind" "+")
int4
((((triple4) -> (rule1 % int4)) ((((((triple4) -> (rule1 % int4))) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Erin is kind.
("Erin" "is" "kind" "+")
int4
((((triple4) -> (rule1 % int5)) ((((((triple4) -> (rule5 % int4))) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Erin is cold.
("Erin" "is" "cold" "+")
int4
Erin is kind.
("Erin" "is" "kind" "+")
int5
Fiona is green.
("Fiona" "is" "green" "+")
((((triple6) -> (rule1 % int2))) -> (rule8 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
((((triple6) -> (rule5 % int2))) -> (rule4 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
((((triple6) -> (rule1 % int2)) triple7) -> (rule2 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
((((triple6) -> (rule1 % int3)) ((triple6) -> (rule6 % int2))) -> (rule2 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
int3
((((triple6) -> (rule1 % int4)) ((((((triple6) -> (rule1 % int4))) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
int3
Fiona is kind.
("Fiona" "is" "kind" "+")
int4
((((triple6) -> (rule1 % int5)) ((((((triple6) -> (rule5 % int4))) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
int3
Fiona is cold.
("Fiona" "is" "cold" "+")
int4
Fiona is kind.
("Fiona" "is" "kind" "+")
int5