Charlie is furry. Charlie is kind. Charlie is young. Gary is blue. Gary is green. Gary is nice. Gary is young. Harry is blue. Harry is nice. Harry is young. If something is green and nice then it is round. Furry, kind things are nice. Round, nice things are green. Round things are kind. If something is young and nice then it is green. If something is blue and round then it is nice. All furry things are blue. Nice, kind things are green.
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is young.
("Gary" "is" "young" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is young.
("Harry" "is" "young" "+")
If something is green and nice then it is round.
((("something" "is" "green" "+") ("something" "is" "nice" "+")) -> ("something" "is" "round" "+"))
Furry, kind things are nice.
((("something" "is" "furry" "+") ("something" "is" "kind" "+")) -> ("something" "is" "nice" "+"))
Round, nice things are green.
((("something" "is" "round" "+") ("something" "is" "nice" "+")) -> ("something" "is" "green" "+"))
Round things are kind.
((("something" "is" "round" "+")) -> ("something" "is" "kind" "+"))
If something is young and nice then it is green.
((("something" "is" "young" "+") ("something" "is" "nice" "+")) -> ("something" "is" "green" "+"))
If something is blue and round then it is nice.
((("something" "is" "blue" "+") ("something" "is" "round" "+")) -> ("something" "is" "nice" "+"))
All furry things are blue.
((("something" "is" "furry" "+")) -> ("something" "is" "blue" "+"))
Nice, kind things are green.
((("something" "is" "nice" "+") ("something" "is" "kind" "+")) -> ("something" "is" "green" "+"))
Harry is blue.
True
1
proof
[(triple8)]
("Harry" "is" "blue" "+")
triple8
Harry is not blue.
False
1
inv-proof
[(triple8)]
("Harry" "is" "blue" "-")
triple8
Harry is green.
True
3
proof
[(((triple10 triple9) -> rule5))]
("Harry" "is" "green" "+")
((triple10 triple9) -> (rule5 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Charlie is not blue.
False
2
inv-proof
[(((triple1) -> rule7))]
("Charlie" "is" "blue" "-")
((triple1) -> (rule7 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Harry is round.
True
5
proof
[(((((triple10 triple9) -> rule5) triple9) -> rule1))]
("Harry" "is" "round" "+")
((((triple10 triple9) -> (rule5 % int2)) triple9) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is not round.
False
5
inv-proof
[(((((triple10 triple9) -> rule5) triple9) -> rule1))]
("Harry" "is" "round" "-")
((((triple10 triple9) -> (rule5 % int2)) triple9) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Charlie is round.
True
9
proof
[(((((triple3 ((triple1 triple2) -> rule2)) -> rule5) ((triple1 triple2) -> rule2)) -> rule1) OR ((((((triple1 triple2) -> rule2) triple2) -> rule8) ((triple1 triple2) -> rule2)) -> rule1))]
("Charlie" "is" "round" "+")
((((triple3 ((triple1 triple2) -> (rule2 % int3))) -> (rule5 % int2)) ((triple1 triple2) -> (rule2 % int3))) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
((((((triple1 triple2) -> (rule2 % int3)) triple2) -> (rule8 % int2)) ((triple1 triple2) -> (rule2 % int3))) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Harry is not kind.
False
6
inv-proof
[(((((((triple10 triple9) -> rule5) triple9) -> rule1)) -> rule4))]
("Harry" "is" "kind" "-")
((((((triple10 triple9) -> (rule5 % int3)) triple9) -> (rule1 % int2))) -> (rule4 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Gary is not furry.
Unknown
inv-random
[@0: Gary is furry.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "furry" "-")
Harry is furry.
Unknown
random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "+")
@0: Charlie is furry.[(triple1)] Charlie is kind.[(triple2)] Charlie is young.[(triple3)] Gary is blue.[(triple4)] Gary is green.[(triple5 OR ((triple7 triple6) -> rule5))] Gary is nice.[(triple6)] Gary is young.[(triple7)] Harry is blue.[(triple8)] Harry is nice.[(triple9)] Harry is young.[(triple10)] @1: Charlie is blue.[(((triple1) -> rule7))] Charlie is nice.[(((triple1 triple2) -> rule2))] Gary is round.[(((triple5 triple6) -> rule1) OR ((((triple7 triple6) -> rule5) triple6) -> rule1))] Harry is green.[(((triple10 triple9) -> rule5))] @2: Charlie is green.[(((triple3 ((triple1 triple2) -> rule2)) -> rule5) OR ((((triple1 triple2) -> rule2) triple2) -> rule8))] Gary is kind.[(((((triple5 triple6) -> rule1)) -> rule4) OR ((((((triple7 triple6) -> rule5) triple6) -> rule1)) -> rule4))] Harry is round.[(((((triple10 triple9) -> rule5) triple9) -> rule1))] @3: Charlie is round.[(((((triple3 ((triple1 triple2) -> rule2)) -> rule5) ((triple1 triple2) -> rule2)) -> rule1) OR ((((((triple1 triple2) -> rule2) triple2) -> rule8) ((triple1 triple2) -> rule2)) -> rule1))] Harry is kind.[(((((((triple10 triple9) -> rule5) triple9) -> rule1)) -> rule4))]
Charlie is furry.
("Charlie" "is" "furry" "+")
triple1
Charlie is kind.
("Charlie" "is" "kind" "+")
triple2
Charlie is young.
("Charlie" "is" "young" "+")
triple3
Gary is blue.
("Gary" "is" "blue" "+")
triple4
Gary is green.
("Gary" "is" "green" "+")
triple5
((triple7 triple6) -> (rule5 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
triple6
Gary is young.
("Gary" "is" "young" "+")
triple7
Harry is blue.
("Harry" "is" "blue" "+")
triple8
Harry is nice.
("Harry" "is" "nice" "+")
triple9
Harry is young.
("Harry" "is" "young" "+")
triple10
Charlie is blue.
("Charlie" "is" "blue" "+")
((triple1) -> (rule7 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
((triple1 triple2) -> (rule2 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
((triple5 triple6) -> (rule1 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
((((triple7 triple6) -> (rule5 % int2)) triple6) -> (rule1 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
((triple10 triple9) -> (rule5 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
((triple3 ((triple1 triple2) -> (rule2 % int2))) -> (rule5 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
((((triple1 triple2) -> (rule2 % int2)) triple2) -> (rule8 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
((((triple5 triple6) -> (rule1 % int2))) -> (rule4 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
((((((triple7 triple6) -> (rule5 % int3)) triple6) -> (rule1 % int2))) -> (rule4 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
Harry is round.
("Harry" "is" "round" "+")
((((triple10 triple9) -> (rule5 % int2)) triple9) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
((((triple3 ((triple1 triple2) -> (rule2 % int3))) -> (rule5 % int2)) ((triple1 triple2) -> (rule2 % int3))) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
((((((triple1 triple2) -> (rule2 % int3)) triple2) -> (rule8 % int2)) ((triple1 triple2) -> (rule2 % int3))) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Harry is kind.
("Harry" "is" "kind" "+")
((((((triple10 triple9) -> (rule5 % int3)) triple9) -> (rule1 % int2))) -> (rule4 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3