Anne is green. Anne is white. Dave is furry. Dave is kind. Dave is smart. Dave is white. Erin is furry. Erin is green. Erin is red. Erin is smart. Erin is white. Erin is young. Fiona is furry. Fiona is green. Fiona is red. Fiona is young. Green things are smart. If Fiona is red and Fiona is young then Fiona is smart. If something is smart then it is white. Kind things are green. If something is white and green then it is young. If something is white and kind then it is smart.
Anne is green.
("Anne" "is" "green" "+")
Anne is white.
("Anne" "is" "white" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is white.
("Dave" "is" "white" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is white.
("Erin" "is" "white" "+")
Erin is young.
("Erin" "is" "young" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Fiona is young.
("Fiona" "is" "young" "+")
Green things are smart.
((("something" "is" "green" "+")) -> ("something" "is" "smart" "+"))
If Fiona is red and Fiona is young then Fiona is smart.
((("Fiona" "is" "red" "+") ("Fiona" "is" "young" "+")) -> ("Fiona" "is" "smart" "+"))
If something is smart then it is white.
((("something" "is" "smart" "+")) -> ("something" "is" "white" "+"))
Kind things are green.
((("something" "is" "kind" "+")) -> ("something" "is" "green" "+"))
If something is white and green then it is young.
((("something" "is" "white" "+") ("something" "is" "green" "+")) -> ("something" "is" "young" "+"))
If something is white and kind then it is smart.
((("something" "is" "white" "+") ("something" "is" "kind" "+")) -> ("something" "is" "smart" "+"))
Erin is green.
True
1
proof
[(triple8)]
("Erin" "is" "green" "+")
triple8
Dave is not white.
False
1
inv-proof
[(triple6 OR ((triple5) -> rule3) OR ((((((triple4) -> rule4)) -> rule1)) -> rule3))]
("Dave" "is" "white" "-")
triple6
((triple5) -> (rule3 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
((((((triple4) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Dave is green.
True
2
proof
[(((triple4) -> rule4))]
("Dave" "is" "green" "+")
((triple4) -> (rule4 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Anne is not smart.
False
2
inv-proof
[(((triple1) -> rule1))]
("Anne" "is" "smart" "-")
((triple1) -> (rule1 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Dave is young.
True
4
proof
[(((triple6 ((triple4) -> rule4)) -> rule5) OR ((((triple5) -> rule3) ((triple4) -> rule4)) -> rule5) OR ((((((((triple4) -> rule4)) -> rule1)) -> rule3) ((triple4) -> rule4)) -> rule5))]
("Dave" "is" "young" "+")
((triple6 ((triple4) -> (rule4 % int2))) -> (rule5 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
((((triple5) -> (rule3 % int3)) ((triple4) -> (rule4 % int2))) -> (rule5 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
((((((((triple4) -> (rule4 % int4))) -> (rule1 % int3))) -> (rule3 % int2)) ((triple4) -> (rule4 % int4))) -> (rule5 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Dave is green.
("Dave" "is" "green" "+")
int4
Fiona is not white.
False
3
inv-proof
[(((((triple14) -> rule1)) -> rule3) OR ((((triple15 triple16) -> rule2)) -> rule3))]
("Fiona" "is" "white" "-")
((((triple14) -> (rule1 % int2))) -> (rule3 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
((((triple15 triple16) -> (rule2 % int2))) -> (rule3 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Dave is not red.
Unknown
inv-random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "-")
Anne is furry.
Unknown
random
[@0: Anne is furry.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "furry" "+")
Fiona is not kind.
Unknown
inv-random
[@0: Fiona is kind.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "kind" "-")
Anne is kind.
Unknown
random
[@0: Anne is kind.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "kind" "+")
Erin is not kind.
Unknown
inv-random
[@0: Erin is kind.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "kind" "-")
Anne is red.
Unknown
random
[@0: Anne is red.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "red" "+")
@0: Anne is green.[(triple1)] Anne is white.[(triple2 OR ((((triple1) -> rule1)) -> rule3))] Dave is furry.[(triple3)] Dave is kind.[(triple4)] Dave is smart.[(triple5 OR ((triple6 triple4) -> rule6) OR ((((triple4) -> rule4)) -> rule1))] Dave is white.[(triple6 OR ((triple5) -> rule3) OR ((((((triple4) -> rule4)) -> rule1)) -> rule3))] Erin is furry.[(triple7)] Erin is green.[(triple8)] Erin is red.[(triple9)] Erin is smart.[(triple10 OR ((triple8) -> rule1))] Erin is white.[(triple11 OR ((triple10) -> rule3) OR ((((triple8) -> rule1)) -> rule3))] Erin is young.[(triple12 OR ((triple11 triple8) -> rule5) OR ((((triple10) -> rule3) triple8) -> rule5) OR ((((((triple8) -> rule1)) -> rule3) triple8) -> rule5))] Fiona is furry.[(triple13)] Fiona is green.[(triple14)] Fiona is red.[(triple15)] Fiona is young.[(triple16 OR ((((((triple14) -> rule1)) -> rule3) triple14) -> rule5))] @1: Anne is smart.[(((triple1) -> rule1))] Anne is young.[(((triple2 triple1) -> rule5) OR ((((((triple1) -> rule1)) -> rule3) triple1) -> rule5))] Dave is green.[(((triple4) -> rule4))] Fiona is smart.[(((triple14) -> rule1) OR ((triple15 triple16) -> rule2))] @2: Dave is young.[(((triple6 ((triple4) -> rule4)) -> rule5) OR ((((triple5) -> rule3) ((triple4) -> rule4)) -> rule5) OR ((((((((triple4) -> rule4)) -> rule1)) -> rule3) ((triple4) -> rule4)) -> rule5))] Fiona is white.[(((((triple14) -> rule1)) -> rule3) OR ((((triple15 triple16) -> rule2)) -> rule3))]
Anne is green.
("Anne" "is" "green" "+")
triple1
Anne is white.
("Anne" "is" "white" "+")
triple2
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
triple3
Dave is kind.
("Dave" "is" "kind" "+")
triple4
Dave is smart.
("Dave" "is" "smart" "+")
triple5
((triple6 triple4) -> (rule6 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
((((triple4) -> (rule4 % int2))) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
triple6
((triple5) -> (rule3 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
((((((triple4) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Erin is furry.
("Erin" "is" "furry" "+")
triple7
Erin is green.
("Erin" "is" "green" "+")
triple8
Erin is red.
("Erin" "is" "red" "+")
triple9
Erin is smart.
("Erin" "is" "smart" "+")
triple10
((triple8) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
triple11
((triple10) -> (rule3 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
((((triple8) -> (rule1 % int2))) -> (rule3 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
triple12
((triple11 triple8) -> (rule5 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
((((triple10) -> (rule3 % int2)) triple8) -> (rule5 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
((((((triple8) -> (rule1 % int3))) -> (rule3 % int2)) triple8) -> (rule5 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Fiona is furry.
("Fiona" "is" "furry" "+")
triple13
Fiona is green.
("Fiona" "is" "green" "+")
triple14
Fiona is red.
("Fiona" "is" "red" "+")
triple15
Fiona is young.
("Fiona" "is" "young" "+")
triple16
((((((triple14) -> (rule1 % int3))) -> (rule3 % int2)) triple14) -> (rule5 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3
Anne is smart.
("Anne" "is" "smart" "+")
((triple1) -> (rule1 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
((triple2 triple1) -> (rule5 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
((((((triple1) -> (rule1 % int3))) -> (rule3 % int2)) triple1) -> (rule5 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Dave is green.
("Dave" "is" "green" "+")
((triple4) -> (rule4 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
((triple14) -> (rule1 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
((triple15 triple16) -> (rule2 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
((triple6 ((triple4) -> (rule4 % int2))) -> (rule5 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
((((triple5) -> (rule3 % int3)) ((triple4) -> (rule4 % int2))) -> (rule5 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
((((((((triple4) -> (rule4 % int4))) -> (rule1 % int3))) -> (rule3 % int2)) ((triple4) -> (rule4 % int4))) -> (rule5 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Dave is green.
("Dave" "is" "green" "+")
int4
Fiona is white.
("Fiona" "is" "white" "+")
((((triple14) -> (rule1 % int2))) -> (rule3 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
((((triple15 triple16) -> (rule2 % int2))) -> (rule3 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2