Bob is red. Bob is rough. Charlie is big. Dave is big. Dave is not blue. Dave is not furry. Dave is red. Dave is not rough. Gary is big. Gary is not blue. If Gary is blue then Gary is nice. If something is furry and not rough then it is red. If Gary is not blue then Gary is furry. All nice things are not furry. If Bob is young then Bob is furry. Blue things are young.
Bob is red.
("Bob" "is" "red" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is not blue.
("Dave" "is" "blue" "-")
Dave is not furry.
("Dave" "is" "furry" "-")
Dave is red.
("Dave" "is" "red" "+")
Dave is not rough.
("Dave" "is" "rough" "-")
Gary is big.
("Gary" "is" "big" "+")
Gary is not blue.
("Gary" "is" "blue" "-")
If Gary is blue then Gary is nice.
((("Gary" "is" "blue" "+")) -> ("Gary" "is" "nice" "+"))
If something is furry and not rough then it is red.
((("something" "is" "furry" "+") ("something" "is" "rough" "~")) -> ("something" "is" "red" "+"))
If Gary is not blue then Gary is furry.
((("Gary" "is" "blue" "~")) -> ("Gary" "is" "furry" "+"))
All nice things are not furry.
((("something" "is" "nice" "+")) -> ("something" "is" "furry" "-"))
If Bob is young then Bob is furry.
((("Bob" "is" "young" "+")) -> ("Bob" "is" "furry" "+"))
Blue things are young.
((("something" "is" "blue" "+")) -> ("something" "is" "young" "+"))
Dave is not blue.
True
1
proof
[(triple5)]
("Dave" "is" "blue" "-")
triple5
Bob is not red.
False
1
inv-proof
[(triple1)]
("Bob" "is" "red" "-")
triple1
Gary is furry.
True
2
proof
[(((triple10) -> rule3))]
("Gary" "is" "furry" "+")
((triple10) -> (rule3 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is not furry.
False
2
inv-proof
[(((triple10) -> rule3))]
("Gary" "is" "furry" "-")
((triple10) -> (rule3 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Charlie is not red.
Unknown
inv-rconc
[@1: Charlie is red.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "red" "-")
Bob is furry.
Unknown
rconc
[@2: Bob is furry.[CWA. Example of deepest failure = (rule5 <- rule6 <- FAIL)]]
("Bob" "is" "furry" "+")
Gary is not rough.
Unknown
inv-random
[@0: Gary is rough.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "rough" "-")
Charlie is nice.
Unknown
random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "+")
@0: Bob is red.[(triple1)] Bob is rough.[(triple2)] Charlie is big.[(triple3)] Dave is big.[(triple4)] Dave is not blue.[(triple5)] Dave is not furry.[(triple6)] Dave is not rough.[(triple8)] Dave is red.[(triple7)] Gary is big.[(triple9)] Gary is not blue.[(triple10)] @1: Gary is furry.[(((triple10) -> rule3))]
Bob is red.
("Bob" "is" "red" "+")
triple1
Bob is rough.
("Bob" "is" "rough" "+")
triple2
Charlie is big.
("Charlie" "is" "big" "+")
triple3
Dave is big.
("Dave" "is" "big" "+")
triple4
Dave is not blue.
("Dave" "is" "blue" "-")
triple5
Dave is not furry.
("Dave" "is" "furry" "-")
triple6
Dave is not rough.
("Dave" "is" "rough" "-")
triple8
Dave is red.
("Dave" "is" "red" "+")
triple7
Gary is big.
("Gary" "is" "big" "+")
triple9
Gary is not blue.
("Gary" "is" "blue" "-")
triple10
Gary is furry.
("Gary" "is" "furry" "+")
((triple10) -> (rule3 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1