Anne is big. Anne is furry. Anne is nice. Anne is quiet. Dave is furry. Dave is green. Dave is nice. Dave is young. Erin is furry. Erin is nice. Harry is big. Harry is red. If Erin is red and Erin is furry then Erin is not young. All quiet, red things are not young. All young, green things are red. All red, big things are quiet. All red, green things are not big. If something is big and not young then it is nice.
Anne is big.
("Anne" "is" "big" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is young.
("Dave" "is" "young" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is red.
("Harry" "is" "red" "+")
If Erin is red and Erin is furry then Erin is not young.
((("Erin" "is" "red" "+") ("Erin" "is" "furry" "+")) -> ("Erin" "is" "young" "-"))
All quiet, red things are not young.
((("something" "is" "quiet" "+") ("something" "is" "red" "+")) -> ("something" "is" "young" "-"))
All young, green things are red.
((("something" "is" "young" "+") ("something" "is" "green" "+")) -> ("something" "is" "red" "+"))
All red, big things are quiet.
((("something" "is" "red" "+") ("something" "is" "big" "+")) -> ("something" "is" "quiet" "+"))
All red, green things are not big.
((("something" "is" "red" "+") ("something" "is" "green" "+")) -> ("something" "is" "big" "-"))
If something is big and not young then it is nice.
((("something" "is" "big" "+") ("something" "is" "young" "~")) -> ("something" "is" "nice" "+"))
Dave is nice.
True
1
proof
[(triple7)]
("Dave" "is" "nice" "+")
triple7
Dave is not furry.
False
1
inv-proof
[(triple5)]
("Dave" "is" "furry" "-")
triple5
Dave is red.
True
3
proof
[(((triple8 triple6) -> rule3))]
("Dave" "is" "red" "+")
((triple8 triple6) -> (rule3 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is not red.
False
3
inv-proof
[(((triple8 triple6) -> rule3))]
("Dave" "is" "red" "-")
((triple8 triple6) -> (rule3 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is not big.
True
5
proof
[(((((triple8 triple6) -> rule3) triple6) -> rule5))]
("Dave" "is" "big" "-")
((((triple8 triple6) -> (rule3 % int2)) triple6) -> (rule5 % int1))
Dave is not big.
("Dave" "is" "big" "-")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Harry is young.
False
5
inv-proof
[(((((triple12 triple11) -> rule4) triple12) -> rule2))]
("Harry" "is" "young" "+")
((((triple12 triple11) -> (rule4 % int2)) triple12) -> (rule2 % int1))
Harry is not young.
("Harry" "is" "young" "-")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is nice.
True
7
proof
[(((triple11 ((((triple12 triple11) -> rule4) triple12) -> rule2)) -> rule6))]
("Harry" "is" "nice" "+")
((triple11 ((((triple12 triple11) -> (rule4 % int3)) triple12) -> (rule2 % int2))) -> (rule6 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is not young.
("Harry" "is" "young" "-")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Harry is not nice.
False
7
inv-proof
[(((triple11 ((((triple12 triple11) -> rule4) triple12) -> rule2)) -> rule6))]
("Harry" "is" "nice" "-")
((triple11 ((((triple12 triple11) -> (rule4 % int3)) triple12) -> (rule2 % int2))) -> (rule6 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is not young.
("Harry" "is" "young" "-")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Erin is not quiet.
Unknown
inv-rconc
[@1: Erin is quiet.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Erin" "is" "quiet" "-")
Dave is quiet.
Unknown
rconc
[@1: Dave is quiet.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Dave" "is" "quiet" "+")
Anne is not red.
Unknown
inv-rconc
[@1: Anne is red.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "red" "-")
Erin is red.
Unknown
rconc
[@1: Erin is red.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Erin" "is" "red" "+")
Anne is not young.
Unknown
inv-random
[@0: Anne is young.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "young" "-")
Erin is big.
Unknown
random
[@0: Erin is big.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "big" "+")
Harry is not furry.
Unknown
inv-random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "-")
Harry is green.
Unknown
random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "+")
@0: Anne is big.[(triple1)] Anne is furry.[(triple2)] Anne is nice.[(triple3)] Anne is quiet.[(triple4)] Dave is furry.[(triple5)] Dave is green.[(triple6)] Dave is nice.[(triple7)] Dave is young.[(triple8)] Erin is furry.[(triple9)] Erin is nice.[(triple10)] Harry is big.[(triple11)] Harry is red.[(triple12)] @1: Dave is red.[(((triple8 triple6) -> rule3))] Harry is quiet.[(((triple12 triple11) -> rule4))] @2: Dave is not big.[(((((triple8 triple6) -> rule3) triple6) -> rule5))] Harry is not young.[(((((triple12 triple11) -> rule4) triple12) -> rule2))] @3: Harry is nice.[(((triple11 ((((triple12 triple11) -> rule4) triple12) -> rule2)) -> rule6))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is furry.
("Anne" "is" "furry" "+")
triple2
Anne is nice.
("Anne" "is" "nice" "+")
triple3
Anne is quiet.
("Anne" "is" "quiet" "+")
triple4
Dave is furry.
("Dave" "is" "furry" "+")
triple5
Dave is green.
("Dave" "is" "green" "+")
triple6
Dave is nice.
("Dave" "is" "nice" "+")
triple7
Dave is young.
("Dave" "is" "young" "+")
triple8
Erin is furry.
("Erin" "is" "furry" "+")
triple9
Erin is nice.
("Erin" "is" "nice" "+")
triple10
Harry is big.
("Harry" "is" "big" "+")
triple11
Harry is red.
("Harry" "is" "red" "+")
triple12
Dave is red.
("Dave" "is" "red" "+")
((triple8 triple6) -> (rule3 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple12 triple11) -> (rule4 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Dave is not big.
("Dave" "is" "big" "-")
((((triple8 triple6) -> (rule3 % int2)) triple6) -> (rule5 % int1))
Dave is not big.
("Dave" "is" "big" "-")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Harry is not young.
("Harry" "is" "young" "-")
((((triple12 triple11) -> (rule4 % int2)) triple12) -> (rule2 % int1))
Harry is not young.
("Harry" "is" "young" "-")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
((triple11 ((((triple12 triple11) -> (rule4 % int3)) triple12) -> (rule2 % int2))) -> (rule6 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is not young.
("Harry" "is" "young" "-")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3