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