Bob is big. Bob is blue. Bob is cold. Bob is furry. Bob is not quiet. Bob is white. Bob is young. Gary is big. Gary is blue. Gary is not cold. Gary is furry. Gary is young. If Bob is quiet then Bob is furry. If something is furry and blue then it is big. All blue, cold things are big. Quiet, blue things are white. All blue things are furry. If something is cold and quiet then it is blue. If something is furry and not blue then it is not young. Cold things are young.
Bob is big.
("Bob" "is" "big" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is not quiet.
("Bob" "is" "quiet" "-")
Bob is white.
("Bob" "is" "white" "+")
Bob is young.
("Bob" "is" "young" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is not cold.
("Gary" "is" "cold" "-")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is young.
("Gary" "is" "young" "+")
If Bob is quiet then Bob is furry.
((("Bob" "is" "quiet" "+")) -> ("Bob" "is" "furry" "+"))
If something is furry and blue then it is big.
((("something" "is" "furry" "+") ("something" "is" "blue" "+")) -> ("something" "is" "big" "+"))
All blue, cold things are big.
((("something" "is" "blue" "+") ("something" "is" "cold" "+")) -> ("something" "is" "big" "+"))
Quiet, blue things are white.
((("something" "is" "quiet" "+") ("something" "is" "blue" "+")) -> ("something" "is" "white" "+"))
All blue things are furry.
((("something" "is" "blue" "+")) -> ("something" "is" "furry" "+"))
If something is cold and quiet then it is blue.
((("something" "is" "cold" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "blue" "+"))
If something is furry and not blue then it is not young.
((("something" "is" "furry" "+") ("something" "is" "blue" "~")) -> ("something" "is" "young" "-"))
Cold things are young.
((("something" "is" "cold" "+")) -> ("something" "is" "young" "+"))
Gary is not cold.
True
1
proof
[(triple10)]
("Gary" "is" "cold" "-")
triple10
Bob is not big.
False
1
inv-proof
[(triple1 OR ((triple2 triple3) -> rule3) OR ((triple4 triple2) -> rule2) OR ((((triple2) -> rule5) triple2) -> rule2))]
("Bob" "is" "big" "-")
triple1
((triple2 triple3) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
((triple4 triple2) -> (rule2 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
((((triple2) -> (rule5 % int2)) triple2) -> (rule2 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Gary is not white.
Unknown
inv-rconc
[@1: Gary is white.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Gary" "is" "white" "-")
Gary is quiet.
Unknown
random
[@0: Gary is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "quiet" "+")
@0: Bob is big.[(triple1 OR ((triple2 triple3) -> rule3) OR ((triple4 triple2) -> rule2) OR ((((triple2) -> rule5) triple2) -> rule2))] Bob is blue.[(triple2)] Bob is cold.[(triple3)] Bob is furry.[(triple4 OR ((triple2) -> rule5))] Bob is not quiet.[(triple5)] Bob is white.[(triple6)] Bob is young.[(triple7 OR ((triple3) -> rule8))] Gary is big.[(triple8 OR ((triple11 triple9) -> rule2) OR ((((triple9) -> rule5) triple9) -> rule2))] Gary is blue.[(triple9)] Gary is furry.[(triple11 OR ((triple9) -> rule5))] Gary is not cold.[(triple10)] Gary is young.[(triple12)]
Bob is big.
("Bob" "is" "big" "+")
triple1
((triple2 triple3) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
((triple4 triple2) -> (rule2 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
((((triple2) -> (rule5 % int2)) triple2) -> (rule2 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
triple2
Bob is cold.
("Bob" "is" "cold" "+")
triple3
Bob is furry.
("Bob" "is" "furry" "+")
triple4
((triple2) -> (rule5 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is not quiet.
("Bob" "is" "quiet" "-")
triple5
Bob is white.
("Bob" "is" "white" "+")
triple6
Bob is young.
("Bob" "is" "young" "+")
triple7
((triple3) -> (rule8 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
triple8
((triple11 triple9) -> (rule2 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
((((triple9) -> (rule5 % int2)) triple9) -> (rule2 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
triple9
Gary is furry.
("Gary" "is" "furry" "+")
triple11
((triple9) -> (rule5 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is not cold.
("Gary" "is" "cold" "-")
triple10
Gary is young.
("Gary" "is" "young" "+")
triple12