Anne is red. Charlie is furry. Charlie is kind. Dave is big. Dave is blue. Dave is green. Fiona is blue. Fiona is furry. Fiona is green. Fiona is kind. Fiona is young. If Anne is red then Anne is big. If something is green and red then it is furry. If something is young then it is green. All big things are kind. Furry things are blue. Kind, red things are green. If something is kind then it is green. Blue, red things are furry.
Anne is red.
("Anne" "is" "red" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is green.
("Dave" "is" "green" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is young.
("Fiona" "is" "young" "+")
If Anne is red then Anne is big.
((("Anne" "is" "red" "+")) -> ("Anne" "is" "big" "+"))
If something is green and red then it is furry.
((("something" "is" "green" "+") ("something" "is" "red" "+")) -> ("something" "is" "furry" "+"))
If something is young then it is green.
((("something" "is" "young" "+")) -> ("something" "is" "green" "+"))
All big things are kind.
((("something" "is" "big" "+")) -> ("something" "is" "kind" "+"))
Furry things are blue.
((("something" "is" "furry" "+")) -> ("something" "is" "blue" "+"))
Kind, red things are green.
((("something" "is" "kind" "+") ("something" "is" "red" "+")) -> ("something" "is" "green" "+"))
If something is kind then it is green.
((("something" "is" "kind" "+")) -> ("something" "is" "green" "+"))
Blue, red things are furry.
((("something" "is" "blue" "+") ("something" "is" "red" "+")) -> ("something" "is" "furry" "+"))
Dave is blue.
True
1
proof
[(triple5)]
("Dave" "is" "blue" "+")
triple5
Fiona is not young.
False
1
inv-proof
[(triple11)]
("Fiona" "is" "young" "-")
triple11
Charlie is blue.
True
2
proof
[(((triple2) -> rule5))]
("Charlie" "is" "blue" "+")
((triple2) -> (rule5 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Dave is not kind.
False
2
inv-proof
[(((triple4) -> rule4))]
("Dave" "is" "kind" "-")
((triple4) -> (rule4 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Anne is kind.
True
3
proof
[(((((triple1) -> rule1)) -> rule4))]
("Anne" "is" "kind" "+")
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is not kind.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule4))]
("Anne" "is" "kind" "-")
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is green.
True
4
proof
[(((((((triple1) -> rule1)) -> rule4)) -> rule7) OR ((((((triple1) -> rule1)) -> rule4) triple1) -> rule6))]
("Anne" "is" "green" "+")
((((((triple1) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
((((((triple1) -> (rule1 % int3))) -> (rule4 % int2)) triple1) -> (rule6 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
Anne is not green.
False
4
inv-proof
[(((((((triple1) -> rule1)) -> rule4)) -> rule7) OR ((((((triple1) -> rule1)) -> rule4) triple1) -> rule6))]
("Anne" "is" "green" "-")
((((((triple1) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
((((((triple1) -> (rule1 % int3))) -> (rule4 % int2)) triple1) -> (rule6 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
Anne is furry.
True
6
proof
[(((((((((triple1) -> rule1)) -> rule4)) -> rule7) triple1) -> rule2) OR ((((((((triple1) -> rule1)) -> rule4) triple1) -> rule6) triple1) -> rule2))]
("Anne" "is" "furry" "+")
((((((((triple1) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule7 % int2)) triple1) -> (rule2 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
Anne is big.
("Anne" "is" "big" "+")
int4
((((((((triple1) -> (rule1 % int4))) -> (rule4 % int3)) triple1) -> (rule6 % int2)) triple1) -> (rule2 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
Anne is big.
("Anne" "is" "big" "+")
int4
Anne is not furry.
False
6
inv-proof
[(((((((((triple1) -> rule1)) -> rule4)) -> rule7) triple1) -> rule2) OR ((((((((triple1) -> rule1)) -> rule4) triple1) -> rule6) triple1) -> rule2))]
("Anne" "is" "furry" "-")
((((((((triple1) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule7 % int2)) triple1) -> (rule2 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
Anne is big.
("Anne" "is" "big" "+")
int4
((((((((triple1) -> (rule1 % int4))) -> (rule4 % int3)) triple1) -> (rule6 % int2)) triple1) -> (rule2 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
Anne is big.
("Anne" "is" "big" "+")
int4
Anne is blue.
True
7
proof
[(((((((((((triple1) -> rule1)) -> rule4)) -> rule7) triple1) -> rule2)) -> rule5) OR ((((((((((triple1) -> rule1)) -> rule4) triple1) -> rule6) triple1) -> rule2)) -> rule5))]
("Anne" "is" "blue" "+")
((((((((((triple1) -> (rule1 % int5))) -> (rule4 % int4))) -> (rule7 % int3)) triple1) -> (rule2 % int2))) -> (rule5 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Anne is kind.
("Anne" "is" "kind" "+")
int4
Anne is big.
("Anne" "is" "big" "+")
int5
((((((((((triple1) -> (rule1 % int5))) -> (rule4 % int4)) triple1) -> (rule6 % int3)) triple1) -> (rule2 % int2))) -> (rule5 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Anne is kind.
("Anne" "is" "kind" "+")
int4
Anne is big.
("Anne" "is" "big" "+")
int5
Anne is not blue.
False
7
inv-proof
[(((((((((((triple1) -> rule1)) -> rule4)) -> rule7) triple1) -> rule2)) -> rule5) OR ((((((((((triple1) -> rule1)) -> rule4) triple1) -> rule6) triple1) -> rule2)) -> rule5))]
("Anne" "is" "blue" "-")
((((((((((triple1) -> (rule1 % int5))) -> (rule4 % int4))) -> (rule7 % int3)) triple1) -> (rule2 % int2))) -> (rule5 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Anne is kind.
("Anne" "is" "kind" "+")
int4
Anne is big.
("Anne" "is" "big" "+")
int5
((((((((((triple1) -> (rule1 % int5))) -> (rule4 % int4)) triple1) -> (rule6 % int3)) triple1) -> (rule2 % int2))) -> (rule5 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Anne is kind.
("Anne" "is" "kind" "+")
int4
Anne is big.
("Anne" "is" "big" "+")
int5
Dave is not furry.
Unknown
inv-rconc
[@1: Dave is furry.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "furry" "-")
Fiona is big.
Unknown
random
[@0: Fiona is big.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "big" "+")
Dave is not red.
Unknown
inv-random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "-")
Charlie is red.
Unknown
random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "+")
Fiona is not red.
Unknown
inv-random
[@0: Fiona is red.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "red" "-")
Anne is young.
Unknown
random
[@0: Anne is young.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "young" "+")
Charlie is not young.
Unknown
inv-random
[@0: Charlie is young.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "young" "-")
Dave is young.
Unknown
random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "+")
@0: Anne is red.[(triple1)] Charlie is furry.[(triple2)] Charlie is kind.[(triple3)] Dave is big.[(triple4)] Dave is blue.[(triple5)] Dave is green.[(triple6 OR ((((triple4) -> rule4)) -> rule7))] Fiona is blue.[(triple7 OR ((triple8) -> rule5))] Fiona is furry.[(triple8)] Fiona is green.[(triple9 OR ((triple10) -> rule7) OR ((triple11) -> rule3))] Fiona is kind.[(triple10)] Fiona is young.[(triple11)] @1: Anne is big.[(((triple1) -> rule1))] Charlie is blue.[(((triple2) -> rule5))] Charlie is green.[(((triple3) -> rule7))] Dave is kind.[(((triple4) -> rule4))] @2: Anne is kind.[(((((triple1) -> rule1)) -> rule4))] @3: Anne is green.[(((((((triple1) -> rule1)) -> rule4)) -> rule7) OR ((((((triple1) -> rule1)) -> rule4) triple1) -> rule6))] @4: Anne is furry.[(((((((((triple1) -> rule1)) -> rule4)) -> rule7) triple1) -> rule2) OR ((((((((triple1) -> rule1)) -> rule4) triple1) -> rule6) triple1) -> rule2))] @5: Anne is blue.[(((((((((((triple1) -> rule1)) -> rule4)) -> rule7) triple1) -> rule2)) -> rule5) OR ((((((((((triple1) -> rule1)) -> rule4) triple1) -> rule6) triple1) -> rule2)) -> rule5))]
Anne is red.
("Anne" "is" "red" "+")
triple1
Charlie is furry.
("Charlie" "is" "furry" "+")
triple2
Charlie is kind.
("Charlie" "is" "kind" "+")
triple3
Dave is big.
("Dave" "is" "big" "+")
triple4
Dave is blue.
("Dave" "is" "blue" "+")
triple5
Dave is green.
("Dave" "is" "green" "+")
triple6
((((triple4) -> (rule4 % int2))) -> (rule7 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
triple7
((triple8) -> (rule5 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
triple8
Fiona is green.
("Fiona" "is" "green" "+")
triple9
((triple10) -> (rule7 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
((triple11) -> (rule3 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
triple10
Fiona is young.
("Fiona" "is" "young" "+")
triple11
Anne is big.
("Anne" "is" "big" "+")
((triple1) -> (rule1 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
((triple2) -> (rule5 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
((triple3) -> (rule7 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
((triple4) -> (rule4 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
((((((triple1) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
((((((triple1) -> (rule1 % int3))) -> (rule4 % int2)) triple1) -> (rule6 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
Anne is furry.
("Anne" "is" "furry" "+")
((((((((triple1) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule7 % int2)) triple1) -> (rule2 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
Anne is big.
("Anne" "is" "big" "+")
int4
((((((((triple1) -> (rule1 % int4))) -> (rule4 % int3)) triple1) -> (rule6 % int2)) triple1) -> (rule2 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
Anne is big.
("Anne" "is" "big" "+")
int4
Anne is blue.
("Anne" "is" "blue" "+")
((((((((((triple1) -> (rule1 % int5))) -> (rule4 % int4))) -> (rule7 % int3)) triple1) -> (rule2 % int2))) -> (rule5 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Anne is kind.
("Anne" "is" "kind" "+")
int4
Anne is big.
("Anne" "is" "big" "+")
int5
((((((((((triple1) -> (rule1 % int5))) -> (rule4 % int4)) triple1) -> (rule6 % int3)) triple1) -> (rule2 % int2))) -> (rule5 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Anne is kind.
("Anne" "is" "kind" "+")
int4
Anne is big.
("Anne" "is" "big" "+")
int5