Bob is big. Bob is blue. Bob is furry. Bob is young. Gary is blue. Gary is white. Gary is young. All young, furry people are white. Blue people are big. If Gary is cold then Gary is young. If someone is white then they are big. If someone is cold then they are big. If Gary is blue and Gary is furry then Gary is cold.
Bob is big.
("Bob" "is" "big" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is young.
("Bob" "is" "young" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is white.
("Gary" "is" "white" "+")
Gary is young.
("Gary" "is" "young" "+")
All young, furry people are white.
((("someone" "is" "young" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "white" "+"))
Blue people are big.
((("someone" "is" "blue" "+")) -> ("someone" "is" "big" "+"))
If Gary is cold then Gary is young.
((("Gary" "is" "cold" "+")) -> ("Gary" "is" "young" "+"))
If someone is white then they are big.
((("someone" "is" "white" "+")) -> ("someone" "is" "big" "+"))
If someone is cold then they are big.
((("someone" "is" "cold" "+")) -> ("someone" "is" "big" "+"))
If Gary is blue and Gary is furry then Gary is cold.
((("Gary" "is" "blue" "+") ("Gary" "is" "furry" "+")) -> ("Gary" "is" "cold" "+"))
Bob is blue.
True
1
proof
[(triple2)]
("Bob" "is" "blue" "+")
triple2
Bob is not young.
False
1
inv-proof
[(triple4)]
("Bob" "is" "young" "-")
triple4
Gary is big.
True
2
proof
[(((triple5) -> rule2) OR ((triple6) -> rule4))]
("Gary" "is" "big" "+")
((triple5) -> (rule2 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
((triple6) -> (rule4 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is not big.
False
2
inv-proof
[(((triple5) -> rule2) OR ((triple6) -> rule4))]
("Gary" "is" "big" "-")
((triple5) -> (rule2 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
((triple6) -> (rule4 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is not cold.
Unknown
inv-rconc
[@1: Gary is cold.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Gary" "is" "cold" "-")
Bob is quiet.
Unknown
random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "+")
Gary is not furry.
Unknown
inv-random
[@0: Gary is furry.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "furry" "-")
Bob is cold.
Unknown
random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "+")
@0: Bob is big.[(triple1 OR ((triple2) -> rule2) OR ((((triple4 triple3) -> rule1)) -> rule4))] Bob is blue.[(triple2)] Bob is furry.[(triple3)] Bob is young.[(triple4)] Gary is blue.[(triple5)] Gary is white.[(triple6)] Gary is young.[(triple7)] @1: Bob is white.[(((triple4 triple3) -> rule1))] Gary is big.[(((triple5) -> rule2) OR ((triple6) -> rule4))]
Bob is big.
("Bob" "is" "big" "+")
triple1
((triple2) -> (rule2 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
((((triple4 triple3) -> (rule1 % int2))) -> (rule4 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
triple2
Bob is furry.
("Bob" "is" "furry" "+")
triple3
Bob is young.
("Bob" "is" "young" "+")
triple4
Gary is blue.
("Gary" "is" "blue" "+")
triple5
Gary is white.
("Gary" "is" "white" "+")
triple6
Gary is young.
("Gary" "is" "young" "+")
triple7
Bob is white.
("Bob" "is" "white" "+")
((triple4 triple3) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
((triple5) -> (rule2 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
((triple6) -> (rule4 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1