Anne is cold. Anne is furry. Anne is kind. Anne is quiet. Anne is round. Anne is smart. Anne is white. Erin is cold. Erin is quiet. Erin is smart. Erin is white. Harry is cold. Harry is furry. Harry is kind. Harry is round. Harry is white. If Harry is smart then Harry is quiet. If Erin is not kind then Erin is not quiet. Cold, round things are white. If something is round and furry then it is white. If something is round then it is smart. If Harry is smart and Harry is cold then Harry is furry.
Anne is cold.
("Anne" "is" "cold" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is round.
("Anne" "is" "round" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Anne is white.
("Anne" "is" "white" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is white.
("Erin" "is" "white" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is white.
("Harry" "is" "white" "+")
If Harry is smart then Harry is quiet.
((("Harry" "is" "smart" "+")) -> ("Harry" "is" "quiet" "+"))
If Erin is not kind then Erin is not quiet.
((("Erin" "is" "kind" "~")) -> ("Erin" "is" "quiet" "-"))
Cold, round things are white.
((("something" "is" "cold" "+") ("something" "is" "round" "+")) -> ("something" "is" "white" "+"))
If something is round and furry then it is white.
((("something" "is" "round" "+") ("something" "is" "furry" "+")) -> ("something" "is" "white" "+"))
If something is round then it is smart.
((("something" "is" "round" "+")) -> ("something" "is" "smart" "+"))
If Harry is smart and Harry is cold then Harry is furry.
((("Harry" "is" "smart" "+") ("Harry" "is" "cold" "+")) -> ("Harry" "is" "furry" "+"))
Anne is round.
True
1
proof
[(triple5)]
("Anne" "is" "round" "+")
triple5
Anne is not furry.
False
1
inv-proof
[(triple2)]
("Anne" "is" "furry" "-")
triple2
Harry is smart.
True
2
proof
[(((triple15) -> rule5))]
("Harry" "is" "smart" "+")
((triple15) -> (rule5 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is not smart.
False
2
inv-proof
[(((triple15) -> rule5))]
("Harry" "is" "smart" "-")
((triple15) -> (rule5 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is quiet.
True
3
proof
[(((((triple15) -> rule5)) -> rule1))]
("Harry" "is" "quiet" "+")
((((triple15) -> (rule5 % int2))) -> (rule1 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is not quiet.
False
3
inv-proof
[(((((triple15) -> rule5)) -> rule1))]
("Harry" "is" "quiet" "-")
((((triple15) -> (rule5 % int2))) -> (rule1 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Erin is not furry.
Unknown
inv-random
[@0: Erin is furry.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "furry" "-")
Erin is kind.
Unknown
random
[@0: Erin is kind.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "kind" "+")
@0: Anne is cold.[(triple1)] Anne is furry.[(triple2)] Anne is kind.[(triple3)] Anne is quiet.[(triple4)] Anne is round.[(triple5)] Anne is smart.[(triple6 OR ((triple5) -> rule5))] Anne is white.[(triple7 OR ((triple1 triple5) -> rule3) OR ((triple5 triple2) -> rule4))] Erin is cold.[(triple8)] Erin is quiet.[(triple9)] Erin is smart.[(triple10)] Erin is white.[(triple11)] Harry is cold.[(triple12)] Harry is furry.[(triple13 OR ((((triple15) -> rule5) triple12) -> rule6))] Harry is kind.[(triple14)] Harry is round.[(triple15)] Harry is white.[(triple16 OR ((triple12 triple15) -> rule3) OR ((triple15 triple13) -> rule4) OR ((triple15 ((((triple15) -> rule5) triple12) -> rule6)) -> rule4))] @1: Harry is smart.[(((triple15) -> rule5))] @2: Harry is quiet.[(((((triple15) -> rule5)) -> rule1))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Anne is furry.
("Anne" "is" "furry" "+")
triple2
Anne is kind.
("Anne" "is" "kind" "+")
triple3
Anne is quiet.
("Anne" "is" "quiet" "+")
triple4
Anne is round.
("Anne" "is" "round" "+")
triple5
Anne is smart.
("Anne" "is" "smart" "+")
triple6
((triple5) -> (rule5 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
triple7
((triple1 triple5) -> (rule3 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
((triple5 triple2) -> (rule4 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
triple8
Erin is quiet.
("Erin" "is" "quiet" "+")
triple9
Erin is smart.
("Erin" "is" "smart" "+")
triple10
Erin is white.
("Erin" "is" "white" "+")
triple11
Harry is cold.
("Harry" "is" "cold" "+")
triple12
Harry is furry.
("Harry" "is" "furry" "+")
triple13
((((triple15) -> (rule5 % int2)) triple12) -> (rule6 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
triple14
Harry is round.
("Harry" "is" "round" "+")
triple15
Harry is white.
("Harry" "is" "white" "+")
triple16
((triple12 triple15) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
((triple15 triple13) -> (rule4 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
((triple15 ((((triple15) -> (rule5 % int3)) triple12) -> (rule6 % int2))) -> (rule4 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
Harry is smart.
("Harry" "is" "smart" "+")
((triple15) -> (rule5 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
((((triple15) -> (rule5 % int2))) -> (rule1 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2