Charlie is quiet. Gary is quiet. Gary is white. All round people are white. All quiet, kind people are red. All round people are white. Quiet people are green. If Gary is quiet and Gary is red then Gary is big. Green people are kind.
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is white.
("Gary" "is" "white" "+")
All round people are white.
((("someone" "is" "round" "+")) -> ("someone" "is" "white" "+"))
All quiet, kind people are red.
((("someone" "is" "quiet" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "red" "+"))
All round people are white.
((("someone" "is" "round" "+")) -> ("someone" "is" "white" "+"))
Quiet people are green.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "green" "+"))
If Gary is quiet and Gary is red then Gary is big.
((("Gary" "is" "quiet" "+") ("Gary" "is" "red" "+")) -> ("Gary" "is" "big" "+"))
Green people are kind.
((("someone" "is" "green" "+")) -> ("someone" "is" "kind" "+"))
Gary is quiet.
True
1
proof
[(triple2)]
("Gary" "is" "quiet" "+")
triple2
Charlie is not quiet.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "quiet" "-")
triple1
Charlie is green.
True
2
proof
[(((triple1) -> rule4))]
("Charlie" "is" "green" "+")
((triple1) -> (rule4 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is not green.
False
2
inv-proof
[(((triple1) -> rule4))]
("Charlie" "is" "green" "-")
((triple1) -> (rule4 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is kind.
True
3
proof
[(((((triple1) -> rule4)) -> rule6))]
("Charlie" "is" "kind" "+")
((((triple1) -> (rule4 % int2))) -> (rule6 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Gary is not kind.
False
3
inv-proof
[(((((triple2) -> rule4)) -> rule6))]
("Gary" "is" "kind" "-")
((((triple2) -> (rule4 % int2))) -> (rule6 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is red.
True
5
proof
[(((triple2 ((((triple2) -> rule4)) -> rule6)) -> rule2))]
("Gary" "is" "red" "+")
((triple2 ((((triple2) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
Gary is not red.
False
5
inv-proof
[(((triple2 ((((triple2) -> rule4)) -> rule6)) -> rule2))]
("Gary" "is" "red" "-")
((triple2 ((((triple2) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
Charlie is not white.
Unknown
inv-rconc
[@1: Charlie is white.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "white" "-")
Charlie is big.
Unknown
random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "+")
Gary is not round.
Unknown
inv-random
[@0: Gary is round.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "round" "-")
Charlie is round.
Unknown
random
[@0: Charlie is round.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "round" "+")
@0: Charlie is quiet.[(triple1)] Gary is quiet.[(triple2)] Gary is white.[(triple3)] @1: Charlie is green.[(((triple1) -> rule4))] Gary is green.[(((triple2) -> rule4))] @2: Charlie is kind.[(((((triple1) -> rule4)) -> rule6))] Gary is kind.[(((((triple2) -> rule4)) -> rule6))] @3: Charlie is red.[(((triple1 ((((triple1) -> rule4)) -> rule6)) -> rule2))] Gary is red.[(((triple2 ((((triple2) -> rule4)) -> rule6)) -> rule2))] @4: Gary is big.[(((triple2 ((triple2 ((((triple2) -> rule4)) -> rule6)) -> rule2)) -> rule5))]
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple1
Gary is quiet.
("Gary" "is" "quiet" "+")
triple2
Gary is white.
("Gary" "is" "white" "+")
triple3
Charlie is green.
("Charlie" "is" "green" "+")
((triple1) -> (rule4 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
((triple2) -> (rule4 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
((((triple1) -> (rule4 % int2))) -> (rule6 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
((((triple2) -> (rule4 % int2))) -> (rule6 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
((triple1 ((((triple1) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
Gary is red.
("Gary" "is" "red" "+")
((triple2 ((((triple2) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
Gary is big.
("Gary" "is" "big" "+")
((triple2 ((triple2 ((((triple2) -> (rule4 % int4))) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3
Gary is green.
("Gary" "is" "green" "+")
int4