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