Anne is big. Anne is smart. Dave is furry. Dave is smart. Erin is blue. Harry is big. Harry is cold. If Erin is green then Erin is big. If someone is furry and cold then they are rough. If someone is blue and not green then they are not rough. If Erin is rough then Erin is blue. If someone is smart then they are cold. All cold people are furry.
Anne is big.
("Anne" "is" "big" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is cold.
("Harry" "is" "cold" "+")
If Erin is green then Erin is big.
((("Erin" "is" "green" "+")) -> ("Erin" "is" "big" "+"))
If someone is furry and cold then they are rough.
((("someone" "is" "furry" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "rough" "+"))
If someone is blue and not green then they are not rough.
((("someone" "is" "blue" "+") ("someone" "is" "green" "~")) -> ("someone" "is" "rough" "-"))
If Erin is rough then Erin is blue.
((("Erin" "is" "rough" "+")) -> ("Erin" "is" "blue" "+"))
If someone is smart then they are cold.
((("someone" "is" "smart" "+")) -> ("someone" "is" "cold" "+"))
All cold people are furry.
((("someone" "is" "cold" "+")) -> ("someone" "is" "furry" "+"))
Anne is big.
True
1
proof
[(triple1)]
("Anne" "is" "big" "+")
triple1
Anne is not smart.
False
1
inv-proof
[(triple2)]
("Anne" "is" "smart" "-")
triple2
Anne is cold.
True
2
proof
[(((triple2) -> rule5))]
("Anne" "is" "cold" "+")
((triple2) -> (rule5 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Harry is not furry.
False
2
inv-proof
[(((triple7) -> rule6))]
("Harry" "is" "furry" "-")
((triple7) -> (rule6 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Anne is furry.
True
3
proof
[(((((triple2) -> rule5)) -> rule6))]
("Anne" "is" "furry" "+")
((((triple2) -> (rule5 % int2))) -> (rule6 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is not furry.
False
3
inv-proof
[(((((triple2) -> rule5)) -> rule6))]
("Anne" "is" "furry" "-")
((((triple2) -> (rule5 % int2))) -> (rule6 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is rough.
True
6
proof
[(((((((triple2) -> rule5)) -> rule6) ((triple2) -> rule5)) -> rule2))]
("Anne" "is" "rough" "+")
((((((triple2) -> (rule5 % int3))) -> (rule6 % int2)) ((triple2) -> (rule5 % int3))) -> (rule2 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Anne is not rough.
False
6
inv-proof
[(((((((triple2) -> rule5)) -> rule6) ((triple2) -> rule5)) -> rule2))]
("Anne" "is" "rough" "-")
((((((triple2) -> (rule5 % int3))) -> (rule6 % int2)) ((triple2) -> (rule5 % int3))) -> (rule2 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Erin is not big.
Unknown
inv-rconc
[@1: Erin is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "big" "-")
Erin is furry.
Unknown
rconc
[@2: Erin is furry.[CWA. Example of deepest failure = (rule6 <- rule5 <- FAIL)]]
("Erin" "is" "furry" "+")
Erin is not rough.
Unknown
inv-rconc
[@2: Erin is rough.[CWA. Example of deepest failure = (rule2 <- rule5 <- FAIL)]]
("Erin" "is" "rough" "-")
Erin is cold.
Unknown
rconc
[@1: Erin is cold.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Erin" "is" "cold" "+")
Erin is not smart.
Unknown
inv-random
[@0: Erin is smart.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "smart" "-")
Dave is big.
Unknown
random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "+")
Erin is not green.
Unknown
inv-random
[@0: Erin is green.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "green" "-")
Dave is green.
Unknown
random
[@0: Dave is green.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "green" "+")
@0: Anne is big.[(triple1)] Anne is smart.[(triple2)] Dave is furry.[(triple3 OR ((((triple4) -> rule5)) -> rule6))] Dave is smart.[(triple4)] Erin is blue.[(triple5)] Harry is big.[(triple6)] Harry is cold.[(triple7)] @1: Anne is cold.[(((triple2) -> rule5))] Dave is cold.[(((triple4) -> rule5))] Harry is furry.[(((triple7) -> rule6))] @2: Anne is furry.[(((((triple2) -> rule5)) -> rule6))] Dave is rough.[(((triple3 ((triple4) -> rule5)) -> rule2) OR ((((((triple4) -> rule5)) -> rule6) ((triple4) -> rule5)) -> rule2))] Harry is rough.[(((((triple7) -> rule6) triple7) -> rule2))] @3: Anne is rough.[(((((((triple2) -> rule5)) -> rule6) ((triple2) -> rule5)) -> rule2))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is smart.
("Anne" "is" "smart" "+")
triple2
Dave is furry.
("Dave" "is" "furry" "+")
triple3
((((triple4) -> (rule5 % int2))) -> (rule6 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
triple4
Erin is blue.
("Erin" "is" "blue" "+")
triple5
Harry is big.
("Harry" "is" "big" "+")
triple6
Harry is cold.
("Harry" "is" "cold" "+")
triple7
Anne is cold.
("Anne" "is" "cold" "+")
((triple2) -> (rule5 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
((triple4) -> (rule5 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
((triple7) -> (rule6 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
((((triple2) -> (rule5 % int2))) -> (rule6 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
((triple3 ((triple4) -> (rule5 % int2))) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
((((((triple4) -> (rule5 % int3))) -> (rule6 % int2)) ((triple4) -> (rule5 % int3))) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3
Harry is rough.
("Harry" "is" "rough" "+")
((((triple7) -> (rule6 % int2)) triple7) -> (rule2 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
((((((triple2) -> (rule5 % int3))) -> (rule6 % int2)) ((triple2) -> (rule5 % int3))) -> (rule2 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3