Bob is blue. Bob is furry. Bob is kind. Bob is round. Bob is not smart. Bob is young. Dave is blue. Dave is red. Dave is round. Dave is young. If Dave is red then Dave is smart. Furry people are round.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is not smart.
("Bob" "is" "smart" "-")
Bob is young.
("Bob" "is" "young" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is young.
("Dave" "is" "young" "+")
If Dave is red then Dave is smart.
((("Dave" "is" "red" "+")) -> ("Dave" "is" "smart" "+"))
Furry people are round.
((("someone" "is" "furry" "+")) -> ("someone" "is" "round" "+"))
Bob is kind.
True
1
proof
[(triple3)]
("Bob" "is" "kind" "+")
triple3
Dave is not round.
False
1
inv-proof
[(triple9)]
("Dave" "is" "round" "-")
triple9
Dave is smart.
True
2
proof
[(((triple8) -> rule1))]
("Dave" "is" "smart" "+")
((triple8) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is not smart.
False
2
inv-proof
[(((triple8) -> rule1))]
("Dave" "is" "smart" "-")
((triple8) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is not furry.
Unknown
inv-random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "-")
Bob is red.
Unknown
random
[@0: Bob is red.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "red" "+")
@0: Bob is blue.[(triple1)] Bob is furry.[(triple2)] Bob is kind.[(triple3)] Bob is not smart.[(triple5)] Bob is round.[(triple4 OR ((triple2) -> rule2))] Bob is young.[(triple6)] Dave is blue.[(triple7)] Dave is red.[(triple8)] Dave is round.[(triple9)] Dave is young.[(triple10)] @1: Dave is smart.[(((triple8) -> rule1))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is furry.
("Bob" "is" "furry" "+")
triple2
Bob is kind.
("Bob" "is" "kind" "+")
triple3
Bob is not smart.
("Bob" "is" "smart" "-")
triple5
Bob is round.
("Bob" "is" "round" "+")
triple4
((triple2) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
triple6
Dave is blue.
("Dave" "is" "blue" "+")
triple7
Dave is red.
("Dave" "is" "red" "+")
triple8
Dave is round.
("Dave" "is" "round" "+")
triple9
Dave is young.
("Dave" "is" "young" "+")
triple10
Dave is smart.
("Dave" "is" "smart" "+")
((triple8) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1