Anne is quiet. Anne is white. Erin is big. Erin is furry. Gary is quiet. Gary is not white. Harry is kind. If Anne is red then Anne is not cold. All big things are quiet. If something is big then it is quiet. If Gary is cold and Gary is big then Gary is not red. Big, quiet things are cold. If something is furry and not kind then it is cold. If Erin is quiet and Erin is cold then Erin is white. If something is white and not quiet then it is furry.
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is white.
("Anne" "is" "white" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is not white.
("Gary" "is" "white" "-")
Harry is kind.
("Harry" "is" "kind" "+")
If Anne is red then Anne is not cold.
((("Anne" "is" "red" "+")) -> ("Anne" "is" "cold" "-"))
All big things are quiet.
((("something" "is" "big" "+")) -> ("something" "is" "quiet" "+"))
If something is big then it is quiet.
((("something" "is" "big" "+")) -> ("something" "is" "quiet" "+"))
If Gary is cold and Gary is big then Gary is not red.
((("Gary" "is" "cold" "+") ("Gary" "is" "big" "+")) -> ("Gary" "is" "red" "-"))
Big, quiet things are cold.
((("something" "is" "big" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "cold" "+"))
If something is furry and not kind then it is cold.
((("something" "is" "furry" "+") ("something" "is" "kind" "~")) -> ("something" "is" "cold" "+"))
If Erin is quiet and Erin is cold then Erin is white.
((("Erin" "is" "quiet" "+") ("Erin" "is" "cold" "+")) -> ("Erin" "is" "white" "+"))
If something is white and not quiet then it is furry.
((("something" "is" "white" "+") ("something" "is" "quiet" "~")) -> ("something" "is" "furry" "+"))
Anne is white.
True
1
proof
[(triple2)]
("Anne" "is" "white" "+")
triple2
Gary is white.
False
1
inv-proof
[(triple6)]
("Gary" "is" "white" "+")
triple6
Erin is quiet.
True
2
proof
[(((triple3) -> rule2) OR ((triple3) -> rule3))]
("Erin" "is" "quiet" "+")
((triple3) -> (rule2 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
((triple3) -> (rule3 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is not quiet.
False
2
inv-proof
[(((triple3) -> rule2) OR ((triple3) -> rule3))]
("Erin" "is" "quiet" "-")
((triple3) -> (rule2 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
((triple3) -> (rule3 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is cold.
True
4
proof
[(((triple3 ((triple3) -> rule2)) -> rule5) OR ((triple3 ((triple3) -> rule3)) -> rule5))]
("Erin" "is" "cold" "+")
((triple3 ((triple3) -> (rule2 % int2))) -> (rule5 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
((triple3 ((triple3) -> (rule3 % int2))) -> (rule5 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is not cold.
False
4
inv-proof
[(((triple3 ((triple3) -> rule2)) -> rule5) OR ((triple3 ((triple3) -> rule3)) -> rule5))]
("Erin" "is" "cold" "-")
((triple3 ((triple3) -> (rule2 % int2))) -> (rule5 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
((triple3 ((triple3) -> (rule3 % int2))) -> (rule5 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is white.
True
7
proof
[(((((triple3) -> rule2) ((triple3 ((triple3) -> rule2)) -> rule5)) -> rule7) OR ((((triple3) -> rule2) ((triple3 ((triple3) -> rule3)) -> rule5)) -> rule7) OR ((((triple3) -> rule3) ((triple3 ((triple3) -> rule2)) -> rule5)) -> rule7) OR ((((triple3) -> rule3) ((triple3 ((triple3) -> rule3)) -> rule5)) -> rule7))]
("Erin" "is" "white" "+")
((((triple3) -> (rule2 % int3)) ((triple3 ((triple3) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
((((triple3) -> (rule2 % int3)) ((triple3 ((triple3) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
((((triple3) -> (rule3 % int3)) ((triple3 ((triple3) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
((((triple3) -> (rule3 % int3)) ((triple3 ((triple3) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
Erin is not white.
False
7
inv-proof
[(((((triple3) -> rule2) ((triple3 ((triple3) -> rule2)) -> rule5)) -> rule7) OR ((((triple3) -> rule2) ((triple3 ((triple3) -> rule3)) -> rule5)) -> rule7) OR ((((triple3) -> rule3) ((triple3 ((triple3) -> rule2)) -> rule5)) -> rule7) OR ((((triple3) -> rule3) ((triple3 ((triple3) -> rule3)) -> rule5)) -> rule7))]
("Erin" "is" "white" "-")
((((triple3) -> (rule2 % int3)) ((triple3 ((triple3) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
((((triple3) -> (rule2 % int3)) ((triple3 ((triple3) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
((((triple3) -> (rule3 % int3)) ((triple3 ((triple3) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
((((triple3) -> (rule3 % int3)) ((triple3 ((triple3) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
Harry is not quiet.
Unknown
inv-rconc
[@1: Harry is quiet.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "quiet" "-")
Anne is furry.
Unknown
rconc
[@1: Anne is furry.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Anne" "is" "furry" "+")
Harry is not furry.
Unknown
inv-rconc
[@1: Harry is furry.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Harry" "is" "furry" "-")
Gary is cold.
Unknown
rconc
[@1: Gary is cold.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Gary" "is" "cold" "+")
Anne is not kind.
Unknown
inv-random
[@0: Anne is kind.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "kind" "-")
Erin is kind.
Unknown
random
[@0: Erin is kind.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "kind" "+")
Harry is not big.
Unknown
inv-random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "-")
Gary is red.
Unknown
random
[@0: Gary is red.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "red" "+")
@0: Anne is quiet.[(triple1)] Anne is white.[(triple2)] Erin is big.[(triple3)] Erin is furry.[(triple4)] Gary is not white.[(triple6)] Gary is quiet.[(triple5)] Harry is kind.[(triple7)] @1: Erin is quiet.[(((triple3) -> rule2) OR ((triple3) -> rule3))] @2: Erin is cold.[(((triple3 ((triple3) -> rule2)) -> rule5) OR ((triple3 ((triple3) -> rule3)) -> rule5))] @3: Erin is white.[(((((triple3) -> rule2) ((triple3 ((triple3) -> rule2)) -> rule5)) -> rule7) OR ((((triple3) -> rule2) ((triple3 ((triple3) -> rule3)) -> rule5)) -> rule7) OR ((((triple3) -> rule3) ((triple3 ((triple3) -> rule2)) -> rule5)) -> rule7) OR ((((triple3) -> rule3) ((triple3 ((triple3) -> rule3)) -> rule5)) -> rule7))]
Anne is quiet.
("Anne" "is" "quiet" "+")
triple1
Anne is white.
("Anne" "is" "white" "+")
triple2
Erin is big.
("Erin" "is" "big" "+")
triple3
Erin is furry.
("Erin" "is" "furry" "+")
triple4
Gary is not white.
("Gary" "is" "white" "-")
triple6
Gary is quiet.
("Gary" "is" "quiet" "+")
triple5
Harry is kind.
("Harry" "is" "kind" "+")
triple7
Erin is quiet.
("Erin" "is" "quiet" "+")
((triple3) -> (rule2 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
((triple3) -> (rule3 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
((triple3 ((triple3) -> (rule2 % int2))) -> (rule5 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
((triple3 ((triple3) -> (rule3 % int2))) -> (rule5 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
((((triple3) -> (rule2 % int3)) ((triple3 ((triple3) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
((((triple3) -> (rule2 % int3)) ((triple3 ((triple3) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
((((triple3) -> (rule3 % int3)) ((triple3 ((triple3) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
((((triple3) -> (rule3 % int3)) ((triple3 ((triple3) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3