Anne is not big. Charlie is young. Gary is not big. All quiet people are red. If someone is young then they are quiet.
Anne is not big.
("Anne" "is" "big" "-")
Charlie is young.
("Charlie" "is" "young" "+")
Gary is not big.
("Gary" "is" "big" "-")
All quiet people are red.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "red" "+"))
If someone is young then they are quiet.
((("someone" "is" "young" "+")) -> ("someone" "is" "quiet" "+"))
Anne is not big.
True
1
proof
[(triple1)]
("Anne" "is" "big" "-")
triple1
Anne is big.
False
1
inv-proof
[(triple1)]
("Anne" "is" "big" "+")
triple1
Charlie is quiet.
True
2
proof
[(((triple2) -> rule2))]
("Charlie" "is" "quiet" "+")
((triple2) -> (rule2 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is not quiet.
False
2
inv-proof
[(((triple2) -> rule2))]
("Charlie" "is" "quiet" "-")
((triple2) -> (rule2 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is red.
True
3
proof
[(((((triple2) -> rule2)) -> rule1))]
("Charlie" "is" "red" "+")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is not red.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule1))]
("Charlie" "is" "red" "-")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Gary is not quiet.
Unknown
inv-rconc
[@1: Gary is quiet.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "quiet" "-")
Gary is red.
Unknown
rconc
[@2: Gary is red.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Gary" "is" "red" "+")
Anne is not red.
Unknown
inv-rconc
[@2: Anne is red.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Anne" "is" "red" "-")
Gary is white.
Unknown
random
[@0: Gary is white.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "white" "+")
Charlie is not white.
Unknown
inv-random
[@0: Charlie is white.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "white" "-")
Anne is nice.
Unknown
random
[@0: Anne is nice.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "nice" "+")
@0: Anne is not big.[(triple1)] Charlie is young.[(triple2)] Gary is not big.[(triple3)] @1: Charlie is quiet.[(((triple2) -> rule2))] @2: Charlie is red.[(((((triple2) -> rule2)) -> rule1))]
Anne is not big.
("Anne" "is" "big" "-")
triple1
Charlie is young.
("Charlie" "is" "young" "+")
triple2
Gary is not big.
("Gary" "is" "big" "-")
triple3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((triple2) -> (rule2 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2