Anne is red. Charlie is cold. Charlie is quiet. Charlie is red. Charlie is round. Harry is furry. Harry is kind. All kind, furry things are round. Red things are furry. If Harry is kind then Harry is nice. Nice, quiet things are furry. All furry things are kind. If Anne is furry then Anne is cold.
Anne is red.
("Anne" "is" "red" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is kind.
("Harry" "is" "kind" "+")
All kind, furry things are round.
((("something" "is" "kind" "+") ("something" "is" "furry" "+")) -> ("something" "is" "round" "+"))
Red things are furry.
((("something" "is" "red" "+")) -> ("something" "is" "furry" "+"))
If Harry is kind then Harry is nice.
((("Harry" "is" "kind" "+")) -> ("Harry" "is" "nice" "+"))
Nice, quiet things are furry.
((("something" "is" "nice" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "furry" "+"))
All furry things are kind.
((("something" "is" "furry" "+")) -> ("something" "is" "kind" "+"))
If Anne is furry then Anne is cold.
((("Anne" "is" "furry" "+")) -> ("Anne" "is" "cold" "+"))
Charlie is quiet.
True
1
proof
[(triple3)]
("Charlie" "is" "quiet" "+")
triple3
Anne is not red.
False
1
inv-proof
[(triple1)]
("Anne" "is" "red" "-")
triple1
Harry is round.
True
3
proof
[(((triple7 triple6) -> rule1) OR ((((triple6) -> rule5) triple6) -> rule1))]
("Harry" "is" "round" "+")
((triple7 triple6) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
((((triple6) -> (rule5 % int2)) triple6) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is not nice.
False
2
inv-proof
[(((triple7) -> rule3) OR ((((triple6) -> rule5)) -> rule3))]
("Harry" "is" "nice" "-")
((triple7) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
((((triple6) -> (rule5 % int2))) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Anne is cold.
True
3
proof
[(((((triple1) -> rule2)) -> rule6))]
("Anne" "is" "cold" "+")
((((triple1) -> (rule2 % int2))) -> (rule6 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is not kind.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule5))]
("Anne" "is" "kind" "-")
((((triple1) -> (rule2 % int2))) -> (rule5 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is round.
True
6
proof
[(((((((triple1) -> rule2)) -> rule5) ((triple1) -> rule2)) -> rule1))]
("Anne" "is" "round" "+")
((((((triple1) -> (rule2 % int3))) -> (rule5 % int2)) ((triple1) -> (rule2 % int3))) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Anne is not round.
False
6
inv-proof
[(((((((triple1) -> rule2)) -> rule5) ((triple1) -> rule2)) -> rule1))]
("Anne" "is" "round" "-")
((((((triple1) -> (rule2 % int3))) -> (rule5 % int2)) ((triple1) -> (rule2 % int3))) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Anne is not nice.
Unknown
inv-random
[@0: Anne is nice.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "nice" "-")
Charlie is nice.
Unknown
random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "+")
Harry is not quiet.
Unknown
inv-random
[@0: Harry is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "quiet" "-")
Harry is red.
Unknown
random
[@0: Harry is red.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "red" "+")
Anne is not quiet.
Unknown
inv-random
[@0: Anne is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "quiet" "-")
Harry is cold.
Unknown
random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "+")
@0: Anne is red.[(triple1)] Charlie is cold.[(triple2)] Charlie is quiet.[(triple3)] Charlie is red.[(triple4)] Charlie is round.[(triple5 OR ((((((triple4) -> rule2)) -> rule5) ((triple4) -> rule2)) -> rule1))] Harry is furry.[(triple6)] Harry is kind.[(triple7 OR ((triple6) -> rule5))] @1: Anne is furry.[(((triple1) -> rule2))] Charlie is furry.[(((triple4) -> rule2))] Harry is nice.[(((triple7) -> rule3) OR ((((triple6) -> rule5)) -> rule3))] Harry is round.[(((triple7 triple6) -> rule1) OR ((((triple6) -> rule5) triple6) -> rule1))] @2: Anne is cold.[(((((triple1) -> rule2)) -> rule6))] Anne is kind.[(((((triple1) -> rule2)) -> rule5))] Charlie is kind.[(((((triple4) -> rule2)) -> rule5))] @3: Anne is round.[(((((((triple1) -> rule2)) -> rule5) ((triple1) -> rule2)) -> rule1))]
Anne is red.
("Anne" "is" "red" "+")
triple1
Charlie is cold.
("Charlie" "is" "cold" "+")
triple2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple3
Charlie is red.
("Charlie" "is" "red" "+")
triple4
Charlie is round.
("Charlie" "is" "round" "+")
triple5
((((((triple4) -> (rule2 % int3))) -> (rule5 % int2)) ((triple4) -> (rule2 % int3))) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
Harry is furry.
("Harry" "is" "furry" "+")
triple6
Harry is kind.
("Harry" "is" "kind" "+")
triple7
((triple6) -> (rule5 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
((triple1) -> (rule2 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
((triple4) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
((triple7) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
((((triple6) -> (rule5 % int2))) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
((triple7 triple6) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
((((triple6) -> (rule5 % int2)) triple6) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
((((triple1) -> (rule2 % int2))) -> (rule6 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
((((triple1) -> (rule2 % int2))) -> (rule5 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
((((triple4) -> (rule2 % int2))) -> (rule5 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
((((((triple1) -> (rule2 % int3))) -> (rule5 % int2)) ((triple1) -> (rule2 % int3))) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3