Anne is smart. Erin is cold. Erin is not furry. Erin is nice. Erin is not red. Erin is smart. Erin is not white. If someone is nice and cold then they are not rough. All cold people are nice. Rough people are nice. If someone is white and furry then they are smart. If someone is nice and furry then they are smart. If Anne is furry and Anne is red then Anne is not white. All furry people are cold. If Anne is smart then Anne is furry.
Anne is smart.
("Anne" "is" "smart" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is not furry.
("Erin" "is" "furry" "-")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is not red.
("Erin" "is" "red" "-")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is not white.
("Erin" "is" "white" "-")
If someone is nice and cold then they are not rough.
((("someone" "is" "nice" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "rough" "-"))
All cold people are nice.
((("someone" "is" "cold" "+")) -> ("someone" "is" "nice" "+"))
Rough people are nice.
((("someone" "is" "rough" "+")) -> ("someone" "is" "nice" "+"))
If someone is white and furry then they are smart.
((("someone" "is" "white" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "smart" "+"))
If someone is nice and furry then they are smart.
((("someone" "is" "nice" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "smart" "+"))
If Anne is furry and Anne is red then Anne is not white.
((("Anne" "is" "furry" "+") ("Anne" "is" "red" "+")) -> ("Anne" "is" "white" "-"))
All furry people are cold.
((("someone" "is" "furry" "+")) -> ("someone" "is" "cold" "+"))
If Anne is smart then Anne is furry.
((("Anne" "is" "smart" "+")) -> ("Anne" "is" "furry" "+"))
Erin is not furry.
True
1
proof
[(triple3)]
("Erin" "is" "furry" "-")
triple3
Erin is not nice.
False
1
inv-proof
[(triple4 OR ((triple2) -> rule2))]
("Erin" "is" "nice" "-")
triple4
((triple2) -> (rule2 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is not rough.
True
3
proof
[(((triple4 triple2) -> rule1) OR ((((triple2) -> rule2) triple2) -> rule1))]
("Erin" "is" "rough" "-")
((triple4 triple2) -> (rule1 % int1))
Erin is not rough.
("Erin" "is" "rough" "-")
int1
((((triple2) -> (rule2 % int2)) triple2) -> (rule1 % int1))
Erin is not rough.
("Erin" "is" "rough" "-")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Anne is not furry.
False
2
inv-proof
[(((triple1) -> rule8))]
("Anne" "is" "furry" "-")
((triple1) -> (rule8 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is cold.
True
3
proof
[(((((triple1) -> rule8)) -> rule7))]
("Anne" "is" "cold" "+")
((((triple1) -> (rule8 % int2))) -> (rule7 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is not cold.
False
3
inv-proof
[(((((triple1) -> rule8)) -> rule7))]
("Anne" "is" "cold" "-")
((((triple1) -> (rule8 % int2))) -> (rule7 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is nice.
True
4
proof
[(((((((triple1) -> rule8)) -> rule7)) -> rule2))]
("Anne" "is" "nice" "+")
((((((triple1) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Anne is not nice.
False
4
inv-proof
[(((((((triple1) -> rule8)) -> rule7)) -> rule2))]
("Anne" "is" "nice" "-")
((((((triple1) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Anne is not red.
Unknown
inv-random
[@0: Anne is red.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "red" "-")
Anne is white.
Unknown
random
[@0: Anne is white.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "white" "+")
@0: Anne is smart.[(triple1)] Erin is cold.[(triple2)] Erin is nice.[(triple4 OR ((triple2) -> rule2))] Erin is not furry.[(triple3)] Erin is not red.[(triple5)] Erin is not white.[(triple7)] Erin is smart.[(triple6)] @1: Anne is furry.[(((triple1) -> rule8))] Erin is not rough.[(((triple4 triple2) -> rule1) OR ((((triple2) -> rule2) triple2) -> rule1))] @2: Anne is cold.[(((((triple1) -> rule8)) -> rule7))] @3: Anne is nice.[(((((((triple1) -> rule8)) -> rule7)) -> rule2))] @4: Anne is not rough.[(((((((((triple1) -> rule8)) -> rule7)) -> rule2) ((((triple1) -> rule8)) -> rule7)) -> rule1))]
Anne is smart.
("Anne" "is" "smart" "+")
triple1
Erin is cold.
("Erin" "is" "cold" "+")
triple2
Erin is nice.
("Erin" "is" "nice" "+")
triple4
((triple2) -> (rule2 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is not furry.
("Erin" "is" "furry" "-")
triple3
Erin is not red.
("Erin" "is" "red" "-")
triple5
Erin is not white.
("Erin" "is" "white" "-")
triple7
Erin is smart.
("Erin" "is" "smart" "+")
triple6
Anne is furry.
("Anne" "is" "furry" "+")
((triple1) -> (rule8 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Erin is not rough.
("Erin" "is" "rough" "-")
((triple4 triple2) -> (rule1 % int1))
Erin is not rough.
("Erin" "is" "rough" "-")
int1
((((triple2) -> (rule2 % int2)) triple2) -> (rule1 % int1))
Erin is not rough.
("Erin" "is" "rough" "-")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
((((triple1) -> (rule8 % int2))) -> (rule7 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
((((((triple1) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Anne is not rough.
("Anne" "is" "rough" "-")
((((((((triple1) -> (rule8 % int4))) -> (rule7 % int3))) -> (rule2 % int2)) ((((triple1) -> (rule8 % int4))) -> (rule7 % int3))) -> (rule1 % int1))
Anne is not rough.
("Anne" "is" "rough" "-")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Anne is furry.
("Anne" "is" "furry" "+")
int4