Charlie is green. Charlie is not red. Charlie is smart. Gary is not green. Gary is not kind. Gary is not rough. Gary is young. If Gary is kind then Gary is smart. All smart things are rough. Smart things are green. All smart, rough things are kind. If something is red and green then it is young. If something is young then it is not red. All quiet, young things are red. If Gary is quiet and Gary is not rough then Gary is not young.
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is not red.
("Charlie" "is" "red" "-")
Charlie is smart.
("Charlie" "is" "smart" "+")
Gary is not green.
("Gary" "is" "green" "-")
Gary is not kind.
("Gary" "is" "kind" "-")
Gary is not rough.
("Gary" "is" "rough" "-")
Gary is young.
("Gary" "is" "young" "+")
If Gary is kind then Gary is smart.
((("Gary" "is" "kind" "+")) -> ("Gary" "is" "smart" "+"))
All smart things are rough.
((("something" "is" "smart" "+")) -> ("something" "is" "rough" "+"))
Smart things are green.
((("something" "is" "smart" "+")) -> ("something" "is" "green" "+"))
All smart, rough things are kind.
((("something" "is" "smart" "+") ("something" "is" "rough" "+")) -> ("something" "is" "kind" "+"))
If something is red and green then it is young.
((("something" "is" "red" "+") ("something" "is" "green" "+")) -> ("something" "is" "young" "+"))
If something is young then it is not red.
((("something" "is" "young" "+")) -> ("something" "is" "red" "-"))
All quiet, young things are red.
((("something" "is" "quiet" "+") ("something" "is" "young" "+")) -> ("something" "is" "red" "+"))
If Gary is quiet and Gary is not rough then Gary is not young.
((("Gary" "is" "quiet" "+") ("Gary" "is" "rough" "~")) -> ("Gary" "is" "young" "-"))
Charlie is smart.
True
1
proof
[(triple3)]
("Charlie" "is" "smart" "+")
triple3
Gary is rough.
False
1
inv-proof
[(triple6)]
("Gary" "is" "rough" "+")
triple6
Charlie is rough.
True
2
proof
[(((triple3) -> rule2))]
("Charlie" "is" "rough" "+")
((triple3) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is not rough.
False
2
inv-proof
[(((triple3) -> rule2))]
("Charlie" "is" "rough" "-")
((triple3) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is kind.
True
4
proof
[(((triple3 ((triple3) -> rule2)) -> rule4))]
("Charlie" "is" "kind" "+")
((triple3 ((triple3) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is not kind.
False
4
inv-proof
[(((triple3 ((triple3) -> rule2)) -> rule4))]
("Charlie" "is" "kind" "-")
((triple3 ((triple3) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is not young.
Unknown
inv-rconc
[@1: Charlie is young.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Charlie" "is" "young" "-")
Gary is smart.
Unknown
rconc
[@1: Gary is smart.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "smart" "+")
Charlie is not quiet.
Unknown
inv-random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "-")
Gary is quiet.
Unknown
random
[@0: Gary is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "quiet" "+")
@0: Charlie is green.[(triple1 OR ((triple3) -> rule3))] Charlie is not red.[(triple2)] Charlie is smart.[(triple3)] Gary is not green.[(triple4)] Gary is not kind.[(triple5)] Gary is not rough.[(triple6)] Gary is young.[(triple7)] @1: Charlie is rough.[(((triple3) -> rule2))] Gary is not red.[(((triple7) -> rule6))] @2: Charlie is kind.[(((triple3 ((triple3) -> rule2)) -> rule4))]
Charlie is green.
("Charlie" "is" "green" "+")
triple1
((triple3) -> (rule3 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is not red.
("Charlie" "is" "red" "-")
triple2
Charlie is smart.
("Charlie" "is" "smart" "+")
triple3
Gary is not green.
("Gary" "is" "green" "-")
triple4
Gary is not kind.
("Gary" "is" "kind" "-")
triple5
Gary is not rough.
("Gary" "is" "rough" "-")
triple6
Gary is young.
("Gary" "is" "young" "+")
triple7
Charlie is rough.
("Charlie" "is" "rough" "+")
((triple3) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Gary is not red.
("Gary" "is" "red" "-")
((triple7) -> (rule6 % int1))
Gary is not red.
("Gary" "is" "red" "-")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
((triple3 ((triple3) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2