Bob is blue. Bob is furry. Bob is kind. Bob is red. Bob is round. Bob is white. Bob is young. Charlie is blue. Charlie is red. Charlie is white. Dave is furry. Dave is kind. Dave is red. Gary is red. Gary is round. Gary is young. All blue things are round. If something is furry and red then it is round. Blue, red things are white.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is white.
("Bob" "is" "white" "+")
Bob is young.
("Bob" "is" "young" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is red.
("Dave" "is" "red" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is young.
("Gary" "is" "young" "+")
All blue things are round.
((("something" "is" "blue" "+")) -> ("something" "is" "round" "+"))
If something is furry and red then it is round.
((("something" "is" "furry" "+") ("something" "is" "red" "+")) -> ("something" "is" "round" "+"))
Blue, red things are white.
((("something" "is" "blue" "+") ("something" "is" "red" "+")) -> ("something" "is" "white" "+"))
Dave is furry.
True
1
proof
[(triple11)]
("Dave" "is" "furry" "+")
triple11
Charlie is not red.
False
1
inv-proof
[(triple9)]
("Charlie" "is" "red" "-")
triple9
Charlie is round.
True
2
proof
[(((triple8) -> rule1))]
("Charlie" "is" "round" "+")
((triple8) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Dave is not round.
False
3
inv-proof
[(((triple11 triple13) -> rule2))]
("Dave" "is" "round" "-")
((triple11 triple13) -> (rule2 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Gary is not white.
Unknown
inv-rconc
[@1: Gary is white.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "white" "-")
Dave is white.
Unknown
rconc
[@1: Dave is white.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "white" "+")
Charlie is not young.
Unknown
inv-random
[@0: Charlie is young.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "young" "-")
Dave is blue.
Unknown
random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "+")
@0: Bob is blue.[(triple1)] Bob is furry.[(triple2)] Bob is kind.[(triple3)] Bob is red.[(triple4)] Bob is round.[(triple5 OR ((triple1) -> rule1) OR ((triple2 triple4) -> rule2))] Bob is white.[(triple6 OR ((triple1 triple4) -> rule3))] Bob is young.[(triple7)] Charlie is blue.[(triple8)] Charlie is red.[(triple9)] Charlie is white.[(triple10 OR ((triple8 triple9) -> rule3))] Dave is furry.[(triple11)] Dave is kind.[(triple12)] Dave is red.[(triple13)] Gary is red.[(triple14)] Gary is round.[(triple15)] Gary is young.[(triple16)] @1: Charlie is round.[(((triple8) -> rule1))] Dave is round.[(((triple11 triple13) -> rule2))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is furry.
("Bob" "is" "furry" "+")
triple2
Bob is kind.
("Bob" "is" "kind" "+")
triple3
Bob is red.
("Bob" "is" "red" "+")
triple4
Bob is round.
("Bob" "is" "round" "+")
triple5
((triple1) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
((triple2 triple4) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
triple6
((triple1 triple4) -> (rule3 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
triple7
Charlie is blue.
("Charlie" "is" "blue" "+")
triple8
Charlie is red.
("Charlie" "is" "red" "+")
triple9
Charlie is white.
("Charlie" "is" "white" "+")
triple10
((triple8 triple9) -> (rule3 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
triple11
Dave is kind.
("Dave" "is" "kind" "+")
triple12
Dave is red.
("Dave" "is" "red" "+")
triple13
Gary is red.
("Gary" "is" "red" "+")
triple14
Gary is round.
("Gary" "is" "round" "+")
triple15
Gary is young.
("Gary" "is" "young" "+")
triple16
Charlie is round.
("Charlie" "is" "round" "+")
((triple8) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
((triple11 triple13) -> (rule2 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1