Charlie is nice. Charlie is smart. Charlie is white. Charlie is young. Harry is red. Harry is white. Harry is young. If Harry is young and Harry is furry then Harry is green. If something is white then it is furry.
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is white.
("Harry" "is" "white" "+")
Harry is young.
("Harry" "is" "young" "+")
If Harry is young and Harry is furry then Harry is green.
((("Harry" "is" "young" "+") ("Harry" "is" "furry" "+")) -> ("Harry" "is" "green" "+"))
If something is white then it is furry.
((("something" "is" "white" "+")) -> ("something" "is" "furry" "+"))
Charlie is nice.
True
1
proof
[(triple1)]
("Charlie" "is" "nice" "+")
triple1
Harry is not red.
False
1
inv-proof
[(triple5)]
("Harry" "is" "red" "-")
triple5
Harry is furry.
True
2
proof
[(((triple6) -> rule2))]
("Harry" "is" "furry" "+")
((triple6) -> (rule2 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is not furry.
False
2
inv-proof
[(((triple6) -> rule2))]
("Harry" "is" "furry" "-")
((triple6) -> (rule2 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is green.
True
4
proof
[(((triple7 ((triple6) -> rule2)) -> rule1))]
("Harry" "is" "green" "+")
((triple7 ((triple6) -> (rule2 % int2))) -> (rule1 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is not green.
False
4
inv-proof
[(((triple7 ((triple6) -> rule2)) -> rule1))]
("Harry" "is" "green" "-")
((triple7 ((triple6) -> (rule2 % int2))) -> (rule1 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Charlie is not red.
Unknown
inv-random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "-")
Harry is nice.
Unknown
random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "+")
Charlie is not green.
Unknown
inv-random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "-")
Harry is smart.
Unknown
random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "+")
@0: Charlie is nice.[(triple1)] Charlie is smart.[(triple2)] Charlie is white.[(triple3)] Charlie is young.[(triple4)] Harry is red.[(triple5)] Harry is white.[(triple6)] Harry is young.[(triple7)] @1: Charlie is furry.[(((triple3) -> rule2))] Harry is furry.[(((triple6) -> rule2))] @2: Harry is green.[(((triple7 ((triple6) -> rule2)) -> rule1))]
Charlie is nice.
("Charlie" "is" "nice" "+")
triple1
Charlie is smart.
("Charlie" "is" "smart" "+")
triple2
Charlie is white.
("Charlie" "is" "white" "+")
triple3
Charlie is young.
("Charlie" "is" "young" "+")
triple4
Harry is red.
("Harry" "is" "red" "+")
triple5
Harry is white.
("Harry" "is" "white" "+")
triple6
Harry is young.
("Harry" "is" "young" "+")
triple7
Charlie is furry.
("Charlie" "is" "furry" "+")
((triple3) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
((triple6) -> (rule2 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
((triple7 ((triple6) -> (rule2 % int2))) -> (rule1 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2