Charlie is big. Gary is blue. If Charlie is big then Charlie is round. If Gary is big and Gary is blue then Gary is young. If Gary is not red then Gary is big. All red people are blue. If someone is kind and big then they are round. If someone is kind and not round then they are young.
Charlie is big.
("Charlie" "is" "big" "+")
Gary is blue.
("Gary" "is" "blue" "+")
If Charlie is big then Charlie is round.
((("Charlie" "is" "big" "+")) -> ("Charlie" "is" "round" "+"))
If Gary is big and Gary is blue then Gary is young.
((("Gary" "is" "big" "+") ("Gary" "is" "blue" "+")) -> ("Gary" "is" "young" "+"))
If Gary is not red then Gary is big.
((("Gary" "is" "red" "~")) -> ("Gary" "is" "big" "+"))
All red people are blue.
((("someone" "is" "red" "+")) -> ("someone" "is" "blue" "+"))
If someone is kind and big then they are round.
((("someone" "is" "kind" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "round" "+"))
If someone is kind and not round then they are young.
((("someone" "is" "kind" "+") ("someone" "is" "round" "~")) -> ("someone" "is" "young" "+"))
Gary is blue.
True
1
proof
[(triple2)]
("Gary" "is" "blue" "+")
triple2
Charlie is not big.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "big" "-")
triple1
Charlie is round.
True
2
proof
[(((triple1) -> rule1))]
("Charlie" "is" "round" "+")
((triple1) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is not round.
False
2
inv-proof
[(((triple1) -> rule1))]
("Charlie" "is" "round" "-")
((triple1) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is not young.
Unknown
inv-rconc
[@1: Charlie is young.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Charlie" "is" "young" "-")
Charlie is blue.
Unknown
rconc
[@1: Charlie is blue.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Charlie" "is" "blue" "+")
Gary is not red.
Unknown
inv-random
[@0: Gary is red.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "red" "-")
Gary is white.
Unknown
random
[@0: Gary is white.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "white" "+")
@0: Charlie is big.[(triple1)] Gary is blue.[(triple2)] @1: Charlie is round.[(((triple1) -> rule1))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Gary is blue.
("Gary" "is" "blue" "+")
triple2
Charlie is round.
("Charlie" "is" "round" "+")
((triple1) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1