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