Charlie is big. Erin is blue. Gary is red. If Gary is blue and Gary is not red then Gary is big. If something is blue and young then it is furry. All big things are furry. Rough, red things are big. If Charlie is not cold then Charlie is not young. If Gary is furry then Gary is cold.
Charlie is big.
("Charlie" "is" "big" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Gary is red.
("Gary" "is" "red" "+")
If Gary is blue and Gary is not red then Gary is big.
((("Gary" "is" "blue" "+") ("Gary" "is" "red" "~")) -> ("Gary" "is" "big" "+"))
If something is blue and young then it is furry.
((("something" "is" "blue" "+") ("something" "is" "young" "+")) -> ("something" "is" "furry" "+"))
All big things are furry.
((("something" "is" "big" "+")) -> ("something" "is" "furry" "+"))
Rough, red things are big.
((("something" "is" "rough" "+") ("something" "is" "red" "+")) -> ("something" "is" "big" "+"))
If Charlie is not cold then Charlie is not young.
((("Charlie" "is" "cold" "~")) -> ("Charlie" "is" "young" "-"))
If Gary is furry then Gary is cold.
((("Gary" "is" "furry" "+")) -> ("Gary" "is" "cold" "+"))
Gary is red.
True
1
proof
[(triple3)]
("Gary" "is" "red" "+")
triple3
Charlie is not big.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "big" "-")
triple1
Charlie is furry.
True
2
proof
[(((triple1) -> rule3))]
("Charlie" "is" "furry" "+")
((triple1) -> (rule3 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is not furry.
False
2
inv-proof
[(((triple1) -> rule3))]
("Charlie" "is" "furry" "-")
((triple1) -> (rule3 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Gary is not furry.
Unknown
inv-rconc
[@2: Gary is furry.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("Gary" "is" "furry" "-")
Erin is furry.
Unknown
rconc
[@2: Erin is furry.[CWA. Example of deepest failure = (rule3 <- rule4 <- FAIL)]]
("Erin" "is" "furry" "+")
Erin is not rough.
Unknown
inv-random
[@0: Erin is rough.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "rough" "-")
Gary is young.
Unknown
random
[@0: Gary is young.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "young" "+")
@0: Charlie is big.[(triple1)] Erin is blue.[(triple2)] Gary is red.[(triple3)] @1: Charlie is furry.[(((triple1) -> rule3))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Erin is blue.
("Erin" "is" "blue" "+")
triple2
Gary is red.
("Gary" "is" "red" "+")
triple3
Charlie is furry.
("Charlie" "is" "furry" "+")
((triple1) -> (rule3 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1