Charlie is big. Gary is big. Gary is nice. If Charlie is red then Charlie is young. If Charlie is quiet and Charlie is round then Charlie is white. White things are red. All round things are big. If Charlie is young and Charlie is nice then Charlie is white. If something is big and nice then it is quiet.
Charlie is big.
("Charlie" "is" "big" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is nice.
("Gary" "is" "nice" "+")
If Charlie is red then Charlie is young.
((("Charlie" "is" "red" "+")) -> ("Charlie" "is" "young" "+"))
If Charlie is quiet and Charlie is round then Charlie is white.
((("Charlie" "is" "quiet" "+") ("Charlie" "is" "round" "+")) -> ("Charlie" "is" "white" "+"))
White things are red.
((("something" "is" "white" "+")) -> ("something" "is" "red" "+"))
All round things are big.
((("something" "is" "round" "+")) -> ("something" "is" "big" "+"))
If Charlie is young and Charlie is nice then Charlie is white.
((("Charlie" "is" "young" "+") ("Charlie" "is" "nice" "+")) -> ("Charlie" "is" "white" "+"))
If something is big and nice then it is quiet.
((("something" "is" "big" "+") ("something" "is" "nice" "+")) -> ("something" "is" "quiet" "+"))
Gary is big.
True
1
proof
[(triple2)]
("Gary" "is" "big" "+")
triple2
Gary is not nice.
False
1
inv-proof
[(triple3)]
("Gary" "is" "nice" "-")
triple3
Gary is quiet.
True
3
proof
[(((triple2 triple3) -> rule6))]
("Gary" "is" "quiet" "+")
((triple2 triple3) -> (rule6 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is not quiet.
False
3
inv-proof
[(((triple2 triple3) -> rule6))]
("Gary" "is" "quiet" "-")
((triple2 triple3) -> (rule6 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Charlie is not white.
Unknown
inv-rconc
[@1: Charlie is white.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "white" "-")
Charlie is red.
Unknown
rconc
[@2: Charlie is red.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("Charlie" "is" "red" "+")
Gary is not young.
Unknown
inv-random
[@0: Gary is young.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "young" "-")
Gary is round.
Unknown
random
[@0: Gary is round.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "round" "+")
@0: Charlie is big.[(triple1)] Gary is big.[(triple2)] Gary is nice.[(triple3)] @1: Gary is quiet.[(((triple2 triple3) -> rule6))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Gary is big.
("Gary" "is" "big" "+")
triple2
Gary is nice.
("Gary" "is" "nice" "+")
triple3
Gary is quiet.
("Gary" "is" "quiet" "+")
((triple2 triple3) -> (rule6 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1