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