Bob is blue. Bob is furry. Bob is green. Bob is rough. Bob is round. Charlie is blue. Charlie is furry. Charlie is smart. Dave is blue. Dave is green. Dave is rough. Dave is smart. All blue, round people are smart. If someone is smart then they are white.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is round.
("Bob" "is" "round" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is smart.
("Dave" "is" "smart" "+")
All blue, round people are smart.
((("someone" "is" "blue" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "smart" "+"))
If someone is smart then they are white.
((("someone" "is" "smart" "+")) -> ("someone" "is" "white" "+"))
Bob is green.
True
1
proof
[(triple3)]
("Bob" "is" "green" "+")
triple3
Charlie is not smart.
False
1
inv-proof
[(triple8)]
("Charlie" "is" "smart" "-")
triple8
Dave is white.
True
2
proof
[(((triple12) -> rule2))]
("Dave" "is" "white" "+")
((triple12) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is not white.
False
2
inv-proof
[(((triple12) -> rule2))]
("Dave" "is" "white" "-")
((triple12) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Bob is white.
True
4
proof
[(((((triple1 triple5) -> rule1)) -> rule2))]
("Bob" "is" "white" "+")
((((triple1 triple5) -> (rule1 % int2))) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is not white.
False
4
inv-proof
[(((((triple1 triple5) -> rule1)) -> rule2))]
("Bob" "is" "white" "-")
((((triple1 triple5) -> (rule1 % int2))) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Charlie is not round.
Unknown
inv-random
[@0: Charlie is round.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "round" "-")
Dave is round.
Unknown
random
[@0: Dave is round.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "round" "+")
Charlie is not rough.
Unknown
inv-random
[@0: Charlie is rough.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "rough" "-")
Charlie is green.
Unknown
random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "+")
@0: Bob is blue.[(triple1)] Bob is furry.[(triple2)] Bob is green.[(triple3)] Bob is rough.[(triple4)] Bob is round.[(triple5)] Charlie is blue.[(triple6)] Charlie is furry.[(triple7)] Charlie is smart.[(triple8)] Dave is blue.[(triple9)] Dave is green.[(triple10)] Dave is rough.[(triple11)] Dave is smart.[(triple12)] @1: Bob is smart.[(((triple1 triple5) -> rule1))] Charlie is white.[(((triple8) -> rule2))] Dave is white.[(((triple12) -> rule2))] @2: Bob is white.[(((((triple1 triple5) -> rule1)) -> rule2))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is furry.
("Bob" "is" "furry" "+")
triple2
Bob is green.
("Bob" "is" "green" "+")
triple3
Bob is rough.
("Bob" "is" "rough" "+")
triple4
Bob is round.
("Bob" "is" "round" "+")
triple5
Charlie is blue.
("Charlie" "is" "blue" "+")
triple6
Charlie is furry.
("Charlie" "is" "furry" "+")
triple7
Charlie is smart.
("Charlie" "is" "smart" "+")
triple8
Dave is blue.
("Dave" "is" "blue" "+")
triple9
Dave is green.
("Dave" "is" "green" "+")
triple10
Dave is rough.
("Dave" "is" "rough" "+")
triple11
Dave is smart.
("Dave" "is" "smart" "+")
triple12
Bob is smart.
("Bob" "is" "smart" "+")
((triple1 triple5) -> (rule1 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
((triple8) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
((triple12) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
((((triple1 triple5) -> (rule1 % int2))) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2