Charlie is kind. Charlie is not quiet. Charlie is not young. Dave is kind. Dave is quiet. Dave is not red. Harry is cold. Harry is not furry. Harry is kind. Harry is quiet. Harry is red. Harry is young. If something is kind then it is cold. If Dave is quiet and Dave is cold then Dave is young. Smart things are quiet.
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
Charlie is not young.
("Charlie" "is" "young" "-")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is not red.
("Dave" "is" "red" "-")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is not furry.
("Harry" "is" "furry" "-")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is young.
("Harry" "is" "young" "+")
If something is kind then it is cold.
((("something" "is" "kind" "+")) -> ("something" "is" "cold" "+"))
If Dave is quiet and Dave is cold then Dave is young.
((("Dave" "is" "quiet" "+") ("Dave" "is" "cold" "+")) -> ("Dave" "is" "young" "+"))
Smart things are quiet.
((("something" "is" "smart" "+")) -> ("something" "is" "quiet" "+"))
Dave is kind.
True
1
proof
[(triple4)]
("Dave" "is" "kind" "+")
triple4
Charlie is young.
False
1
inv-proof
[(triple3)]
("Charlie" "is" "young" "+")
triple3
Dave is cold.
True
2
proof
[(((triple4) -> rule1))]
("Dave" "is" "cold" "+")
((triple4) -> (rule1 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is not cold.
False
2
inv-proof
[(((triple4) -> rule1))]
("Dave" "is" "cold" "-")
((triple4) -> (rule1 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is young.
True
4
proof
[(((triple5 ((triple4) -> rule1)) -> rule2))]
("Dave" "is" "young" "+")
((triple5 ((triple4) -> (rule1 % int2))) -> (rule2 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is not young.
False
4
inv-proof
[(((triple5 ((triple4) -> rule1)) -> rule2))]
("Dave" "is" "young" "-")
((triple5 ((triple4) -> (rule1 % int2))) -> (rule2 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Charlie is not furry.
Unknown
inv-random
[@0: Charlie is furry.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "furry" "-")
Harry is smart.
Unknown
random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "+")
Charlie is not smart.
Unknown
inv-random
[@0: Charlie is smart.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "smart" "-")
Charlie is red.
Unknown
random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "+")
Dave is not smart.
Unknown
inv-random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "-")
Dave is furry.
Unknown
random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "+")
@0: Charlie is kind.[(triple1)] Charlie is not quiet.[(triple2)] Charlie is not young.[(triple3)] Dave is kind.[(triple4)] Dave is not red.[(triple6)] Dave is quiet.[(triple5)] Harry is cold.[(triple7 OR ((triple9) -> rule1))] Harry is kind.[(triple9)] Harry is not furry.[(triple8)] Harry is quiet.[(triple10)] Harry is red.[(triple11)] Harry is young.[(triple12)] @1: Charlie is cold.[(((triple1) -> rule1))] Dave is cold.[(((triple4) -> rule1))] @2: Dave is young.[(((triple5 ((triple4) -> rule1)) -> rule2))]
Charlie is kind.
("Charlie" "is" "kind" "+")
triple1
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
triple2
Charlie is not young.
("Charlie" "is" "young" "-")
triple3
Dave is kind.
("Dave" "is" "kind" "+")
triple4
Dave is not red.
("Dave" "is" "red" "-")
triple6
Dave is quiet.
("Dave" "is" "quiet" "+")
triple5
Harry is cold.
("Harry" "is" "cold" "+")
triple7
((triple9) -> (rule1 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
triple9
Harry is not furry.
("Harry" "is" "furry" "-")
triple8
Harry is quiet.
("Harry" "is" "quiet" "+")
triple10
Harry is red.
("Harry" "is" "red" "+")
triple11
Harry is young.
("Harry" "is" "young" "+")
triple12
Charlie is cold.
("Charlie" "is" "cold" "+")
((triple1) -> (rule1 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
((triple4) -> (rule1 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
((triple5 ((triple4) -> (rule1 % int2))) -> (rule2 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2