Dave is furry. Dave is kind. Dave is quiet. Dave is young. Erin is blue. Erin is green. Erin is kind. Erin is quiet. Erin is round. Erin is not young. Harry is blue. Harry is green. Harry is quiet. Harry is round. Harry is young. If Dave is green then Dave is quiet. If Harry is blue then Harry is furry.
Dave is furry.
("Dave" "is" "furry" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is young.
("Dave" "is" "young" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is not young.
("Erin" "is" "young" "-")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is young.
("Harry" "is" "young" "+")
If Dave is green then Dave is quiet.
((("Dave" "is" "green" "+")) -> ("Dave" "is" "quiet" "+"))
If Harry is blue then Harry is furry.
((("Harry" "is" "blue" "+")) -> ("Harry" "is" "furry" "+"))
Harry is quiet.
True
1
proof
[(triple13)]
("Harry" "is" "quiet" "+")
triple13
Dave is not quiet.
False
1
inv-proof
[(triple3)]
("Dave" "is" "quiet" "-")
triple3
Harry is furry.
True
2
proof
[(((triple11) -> rule2))]
("Harry" "is" "furry" "+")
((triple11) -> (rule2 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is not furry.
False
2
inv-proof
[(((triple11) -> rule2))]
("Harry" "is" "furry" "-")
((triple11) -> (rule2 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Dave is not round.
Unknown
inv-random
[@0: Dave is round.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "round" "-")
Erin is furry.
Unknown
random
[@0: Erin is furry.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "furry" "+")
Dave is not blue.
Unknown
inv-random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "-")
Harry is kind.
Unknown
random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "+")
@0: Dave is furry.[(triple1)] Dave is kind.[(triple2)] Dave is quiet.[(triple3)] Dave is young.[(triple4)] Erin is blue.[(triple5)] Erin is green.[(triple6)] Erin is kind.[(triple7)] Erin is not young.[(triple10)] Erin is quiet.[(triple8)] Erin is round.[(triple9)] Harry is blue.[(triple11)] Harry is green.[(triple12)] Harry is quiet.[(triple13)] Harry is round.[(triple14)] Harry is young.[(triple15)] @1: Harry is furry.[(((triple11) -> rule2))]
Dave is furry.
("Dave" "is" "furry" "+")
triple1
Dave is kind.
("Dave" "is" "kind" "+")
triple2
Dave is quiet.
("Dave" "is" "quiet" "+")
triple3
Dave is young.
("Dave" "is" "young" "+")
triple4
Erin is blue.
("Erin" "is" "blue" "+")
triple5
Erin is green.
("Erin" "is" "green" "+")
triple6
Erin is kind.
("Erin" "is" "kind" "+")
triple7
Erin is not young.
("Erin" "is" "young" "-")
triple10
Erin is quiet.
("Erin" "is" "quiet" "+")
triple8
Erin is round.
("Erin" "is" "round" "+")
triple9
Harry is blue.
("Harry" "is" "blue" "+")
triple11
Harry is green.
("Harry" "is" "green" "+")
triple12
Harry is quiet.
("Harry" "is" "quiet" "+")
triple13
Harry is round.
("Harry" "is" "round" "+")
triple14
Harry is young.
("Harry" "is" "young" "+")
triple15
Harry is furry.
("Harry" "is" "furry" "+")
((triple11) -> (rule2 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1