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