Bob is blue. Erin is rough. Gary is white. White things are blue. Big, nice things are young. If something is blue and furry then it is big. All blue, white things are big. Big things are furry. If Bob is young and Bob is white then Bob is rough.
Bob is blue.
("Bob" "is" "blue" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Gary is white.
("Gary" "is" "white" "+")
White things are blue.
((("something" "is" "white" "+")) -> ("something" "is" "blue" "+"))
Big, nice things are young.
((("something" "is" "big" "+") ("something" "is" "nice" "+")) -> ("something" "is" "young" "+"))
If something is blue and furry then it is big.
((("something" "is" "blue" "+") ("something" "is" "furry" "+")) -> ("something" "is" "big" "+"))
All blue, white things are big.
((("something" "is" "blue" "+") ("something" "is" "white" "+")) -> ("something" "is" "big" "+"))
Big things are furry.
((("something" "is" "big" "+")) -> ("something" "is" "furry" "+"))
If Bob is young and Bob is white then Bob is rough.
((("Bob" "is" "young" "+") ("Bob" "is" "white" "+")) -> ("Bob" "is" "rough" "+"))
Gary is white.
True
1
proof
[(triple3)]
("Gary" "is" "white" "+")
triple3
Gary is not white.
False
1
inv-proof
[(triple3)]
("Gary" "is" "white" "-")
triple3
Gary is blue.
True
2
proof
[(((triple3) -> rule1))]
("Gary" "is" "blue" "+")
((triple3) -> (rule1 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is not blue.
False
2
inv-proof
[(((triple3) -> rule1))]
("Gary" "is" "blue" "-")
((triple3) -> (rule1 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is big.
True
4
proof
[(((((triple3) -> rule1) triple3) -> rule4))]
("Gary" "is" "big" "+")
((((triple3) -> (rule1 % int2)) triple3) -> (rule4 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is not big.
False
4
inv-proof
[(((((triple3) -> rule1) triple3) -> rule4))]
("Gary" "is" "big" "-")
((((triple3) -> (rule1 % int2)) triple3) -> (rule4 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Bob is not big.
Unknown
inv-rconc
[@3: Bob is big.[CWA. Example of deepest failure = (rule3 <- rule5 <- rule4 <- FAIL)]]
("Bob" "is" "big" "-")
Bob is young.
Unknown
rconc
[@1: Bob is young.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "young" "+")
Gary is not young.
Unknown
inv-rconc
[@1: Gary is young.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "young" "-")
Bob is nice.
Unknown
random
[@0: Bob is nice.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "nice" "+")
Gary is not rough.
Unknown
inv-random
[@0: Gary is rough.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "rough" "-")
Erin is white.
Unknown
random
[@0: Erin is white.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "white" "+")
@0: Bob is blue.[(triple1)] Erin is rough.[(triple2)] Gary is white.[(triple3)] @1: Gary is blue.[(((triple3) -> rule1))] @2: Gary is big.[(((((triple3) -> rule1) triple3) -> rule4))] @3: Gary is furry.[(((((((triple3) -> rule1) triple3) -> rule4)) -> rule5))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Erin is rough.
("Erin" "is" "rough" "+")
triple2
Gary is white.
("Gary" "is" "white" "+")
triple3
Gary is blue.
("Gary" "is" "blue" "+")
((triple3) -> (rule1 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
((((triple3) -> (rule1 % int2)) triple3) -> (rule4 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
((((((triple3) -> (rule1 % int3)) triple3) -> (rule4 % int2))) -> (rule5 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3