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