Bob is blue. Bob is quiet. Bob is red. Bob is round. Bob is white. Dave is big. Dave is red. Dave is round. Dave is smart. Dave is white. Big, quiet things are blue. All big things are quiet.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is white.
("Bob" "is" "white" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is white.
("Dave" "is" "white" "+")
Big, quiet things are blue.
((("something" "is" "big" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "blue" "+"))
All big things are quiet.
((("something" "is" "big" "+")) -> ("something" "is" "quiet" "+"))
Bob is white.
True
1
proof
[(triple5)]
("Bob" "is" "white" "+")
triple5
Bob is not quiet.
False
1
inv-proof
[(triple2)]
("Bob" "is" "quiet" "-")
triple2
Dave is quiet.
True
2
proof
[(((triple6) -> rule2))]
("Dave" "is" "quiet" "+")
((triple6) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is not quiet.
False
2
inv-proof
[(((triple6) -> rule2))]
("Dave" "is" "quiet" "-")
((triple6) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Bob is not smart.
Unknown
inv-random
[@0: Bob is smart.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "smart" "-")
Bob is big.
Unknown
random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "+")
@0: Bob is blue.[(triple1)] Bob is quiet.[(triple2)] Bob is red.[(triple3)] Bob is round.[(triple4)] Bob is white.[(triple5)] Dave is big.[(triple6)] Dave is red.[(triple7)] Dave is round.[(triple8)] Dave is smart.[(triple9)] Dave is white.[(triple10)] @1: Dave is quiet.[(((triple6) -> rule2))] @2: Dave is blue.[(((triple6 ((triple6) -> rule2)) -> rule1))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is quiet.
("Bob" "is" "quiet" "+")
triple2
Bob is red.
("Bob" "is" "red" "+")
triple3
Bob is round.
("Bob" "is" "round" "+")
triple4
Bob is white.
("Bob" "is" "white" "+")
triple5
Dave is big.
("Dave" "is" "big" "+")
triple6
Dave is red.
("Dave" "is" "red" "+")
triple7
Dave is round.
("Dave" "is" "round" "+")
triple8
Dave is smart.
("Dave" "is" "smart" "+")
triple9
Dave is white.
("Dave" "is" "white" "+")
triple10
Dave is quiet.
("Dave" "is" "quiet" "+")
((triple6) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
((triple6 ((triple6) -> (rule2 % int2))) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2