Charlie is big. Charlie is blue. Charlie is green. Charlie is quiet. Charlie is not white. Dave is not green. Dave is nice. Dave is quiet. Dave is not white. Gary is blue. If someone is white then they are nice. All quiet people are not young. If Charlie is white and Charlie is not nice then Charlie is quiet. If someone is blue and not quiet then they are big. All white people are blue. If someone is quiet and not young then they are blue.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is not white.
("Charlie" "is" "white" "-")
Dave is not green.
("Dave" "is" "green" "-")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is not white.
("Dave" "is" "white" "-")
Gary is blue.
("Gary" "is" "blue" "+")
If someone is white then they are nice.
((("someone" "is" "white" "+")) -> ("someone" "is" "nice" "+"))
All quiet people are not young.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "young" "-"))
If Charlie is white and Charlie is not nice then Charlie is quiet.
((("Charlie" "is" "white" "+") ("Charlie" "is" "nice" "~")) -> ("Charlie" "is" "quiet" "+"))
If someone is blue and not quiet then they are big.
((("someone" "is" "blue" "+") ("someone" "is" "quiet" "~")) -> ("someone" "is" "big" "+"))
All white people are blue.
((("someone" "is" "white" "+")) -> ("someone" "is" "blue" "+"))
If someone is quiet and not young then they are blue.
((("someone" "is" "quiet" "+") ("someone" "is" "young" "~")) -> ("someone" "is" "blue" "+"))
Charlie is quiet.
True
1
proof
[(triple4)]
("Charlie" "is" "quiet" "+")
triple4
Dave is not nice.
False
1
inv-proof
[(triple7)]
("Dave" "is" "nice" "-")
triple7
Charlie is not young.
True
2
proof
[(((triple4) -> rule2))]
("Charlie" "is" "young" "-")
((triple4) -> (rule2 % int1))
Charlie is not young.
("Charlie" "is" "young" "-")
int1
Charlie is young.
False
2
inv-proof
[(((triple4) -> rule2))]
("Charlie" "is" "young" "+")
((triple4) -> (rule2 % int1))
Charlie is not young.
("Charlie" "is" "young" "-")
int1
Dave is blue.
True
4
proof
[(((triple8 ((triple8) -> rule2)) -> rule6))]
("Dave" "is" "blue" "+")
((triple8 ((triple8) -> (rule2 % int2))) -> (rule6 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is not young.
("Dave" "is" "young" "-")
int2
Dave is not blue.
False
4
inv-proof
[(((triple8 ((triple8) -> rule2)) -> rule6))]
("Dave" "is" "blue" "-")
((triple8 ((triple8) -> (rule2 % int2))) -> (rule6 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is not young.
("Dave" "is" "young" "-")
int2
Gary is not big.
Unknown
inv-rconc
[@1: Gary is big.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Gary" "is" "big" "-")
Gary is nice.
Unknown
rconc
[@1: Gary is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "nice" "+")
Charlie is not nice.
Unknown
inv-rconc
[@1: Charlie is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "nice" "-")
Gary is white.
Unknown
random
[@0: Gary is white.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "white" "+")
Gary is not green.
Unknown
inv-random
[@0: Gary is green.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "green" "-")
Gary is young.
Unknown
random
[@0: Gary is young.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "young" "+")
@0: Charlie is big.[(triple1)] Charlie is blue.[(triple2 OR ((triple4 ((triple4) -> rule2)) -> rule6))] Charlie is green.[(triple3)] Charlie is not white.[(triple5)] Charlie is quiet.[(triple4)] Dave is nice.[(triple7)] Dave is not green.[(triple6)] Dave is not white.[(triple9)] Dave is quiet.[(triple8)] Gary is blue.[(triple10)] @1: Charlie is not young.[(((triple4) -> rule2))] Dave is not young.[(((triple8) -> rule2))] @2: Dave is blue.[(((triple8 ((triple8) -> rule2)) -> rule6))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Charlie is blue.
("Charlie" "is" "blue" "+")
triple2
((triple4 ((triple4) -> (rule2 % int2))) -> (rule6 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is not young.
("Charlie" "is" "young" "-")
int2
Charlie is green.
("Charlie" "is" "green" "+")
triple3
Charlie is not white.
("Charlie" "is" "white" "-")
triple5
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple4
Dave is nice.
("Dave" "is" "nice" "+")
triple7
Dave is not green.
("Dave" "is" "green" "-")
triple6
Dave is not white.
("Dave" "is" "white" "-")
triple9
Dave is quiet.
("Dave" "is" "quiet" "+")
triple8
Gary is blue.
("Gary" "is" "blue" "+")
triple10
Charlie is not young.
("Charlie" "is" "young" "-")
((triple4) -> (rule2 % int1))
Charlie is not young.
("Charlie" "is" "young" "-")
int1
Dave is not young.
("Dave" "is" "young" "-")
((triple8) -> (rule2 % int1))
Dave is not young.
("Dave" "is" "young" "-")
int1
Dave is blue.
("Dave" "is" "blue" "+")
((triple8 ((triple8) -> (rule2 % int2))) -> (rule6 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is not young.
("Dave" "is" "young" "-")
int2