Anne is big. Anne is cold. Anne is green. Anne is round. Dave is rough. Erin is big. Erin is furry. Erin is white. Fiona is big. Fiona is furry. All big, rough people are round. All furry people are white. Round people are furry. Cold, white people are big. If Erin is round then Erin is white. Green, cold people are furry. All round people are rough. Rough people are cold. Cold people are round.
Anne is big.
("Anne" "is" "big" "+")
Anne is cold.
("Anne" "is" "cold" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is round.
("Anne" "is" "round" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is white.
("Erin" "is" "white" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
All big, rough people are round.
((("someone" "is" "big" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "round" "+"))
All furry people are white.
((("someone" "is" "furry" "+")) -> ("someone" "is" "white" "+"))
Round people are furry.
((("someone" "is" "round" "+")) -> ("someone" "is" "furry" "+"))
Cold, white people are big.
((("someone" "is" "cold" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "big" "+"))
If Erin is round then Erin is white.
((("Erin" "is" "round" "+")) -> ("Erin" "is" "white" "+"))
Green, cold people are furry.
((("someone" "is" "green" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "furry" "+"))
All round people are rough.
((("someone" "is" "round" "+")) -> ("someone" "is" "rough" "+"))
Rough people are cold.
((("someone" "is" "rough" "+")) -> ("someone" "is" "cold" "+"))
Cold people are round.
((("someone" "is" "cold" "+")) -> ("someone" "is" "round" "+"))
Anne is round.
True
1
proof
[(triple4 OR ((triple2) -> rule9))]
("Anne" "is" "round" "+")
triple4
((triple2) -> (rule9 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Fiona is not big.
False
1
inv-proof
[(triple9)]
("Fiona" "is" "big" "-")
triple9
Dave is cold.
True
2
proof
[(((triple5) -> rule8))]
("Dave" "is" "cold" "+")
((triple5) -> (rule8 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is not cold.
False
2
inv-proof
[(((triple5) -> rule8))]
("Dave" "is" "cold" "-")
((triple5) -> (rule8 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Anne is white.
True
3
proof
[(((((triple4) -> rule3)) -> rule2) OR ((((triple3 triple2) -> rule6)) -> rule2) OR ((((((triple2) -> rule9)) -> rule3)) -> rule2) OR ((((triple3 ((((triple4) -> rule7)) -> rule8)) -> rule6)) -> rule2))]
("Anne" "is" "white" "+")
((((triple4) -> (rule3 % int2))) -> (rule2 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
((((triple3 triple2) -> (rule6 % int2))) -> (rule2 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
((((((triple2) -> (rule9 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
((((triple3 ((((triple4) -> (rule7 % int4))) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Anne is rough.
("Anne" "is" "rough" "+")
int4
Anne is not white.
False
3
inv-proof
[(((((triple4) -> rule3)) -> rule2) OR ((((triple3 triple2) -> rule6)) -> rule2) OR ((((((triple2) -> rule9)) -> rule3)) -> rule2) OR ((((triple3 ((((triple4) -> rule7)) -> rule8)) -> rule6)) -> rule2))]
("Anne" "is" "white" "-")
((((triple4) -> (rule3 % int2))) -> (rule2 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
((((triple3 triple2) -> (rule6 % int2))) -> (rule2 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
((((((triple2) -> (rule9 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
((((triple3 ((((triple4) -> (rule7 % int4))) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Anne is rough.
("Anne" "is" "rough" "+")
int4
Dave is furry.
True
4
proof
[(((((((triple5) -> rule8)) -> rule9)) -> rule3))]
("Dave" "is" "furry" "+")
((((((triple5) -> (rule8 % int3))) -> (rule9 % int2))) -> (rule3 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3
Dave is not furry.
False
4
inv-proof
[(((((((triple5) -> rule8)) -> rule9)) -> rule3))]
("Dave" "is" "furry" "-")
((((((triple5) -> (rule8 % int3))) -> (rule9 % int2))) -> (rule3 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3
Dave is white.
True
5
proof
[(((((((((triple5) -> rule8)) -> rule9)) -> rule3)) -> rule2))]
("Dave" "is" "white" "+")
((((((((triple5) -> (rule8 % int4))) -> (rule9 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is cold.
("Dave" "is" "cold" "+")
int4
Dave is not white.
False
5
inv-proof
[(((((((((triple5) -> rule8)) -> rule9)) -> rule3)) -> rule2))]
("Dave" "is" "white" "-")
((((((((triple5) -> (rule8 % int4))) -> (rule9 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is cold.
("Dave" "is" "cold" "+")
int4
Dave is big.
True
8
proof
[(((((triple5) -> rule8) ((((((((triple5) -> rule8)) -> rule9)) -> rule3)) -> rule2)) -> rule4))]
("Dave" "is" "big" "+")
((((triple5) -> (rule8 % int5)) ((((((((triple5) -> (rule8 % int5))) -> (rule9 % int4))) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Dave is round.
("Dave" "is" "round" "+")
int4
Dave is cold.
("Dave" "is" "cold" "+")
int5
Dave is not big.
False
8
inv-proof
[(((((triple5) -> rule8) ((((((((triple5) -> rule8)) -> rule9)) -> rule3)) -> rule2)) -> rule4))]
("Dave" "is" "big" "-")
((((triple5) -> (rule8 % int5)) ((((((((triple5) -> (rule8 % int5))) -> (rule9 % int4))) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Dave is round.
("Dave" "is" "round" "+")
int4
Dave is cold.
("Dave" "is" "cold" "+")
int5
Erin is not round.
Unknown
inv-rconc
[@4: Erin is round.[CWA. Example of deepest failure = (rule1 <- rule7 <- rule9 <- rule8 <- FAIL)]]
("Erin" "is" "round" "-")
Fiona is cold.
Unknown
rconc
[@3: Fiona is cold.[CWA. Example of deepest failure = (rule8 <- rule7 <- rule1 <- FAIL)]]
("Fiona" "is" "cold" "+")
Fiona is not rough.
Unknown
inv-rconc
[@3: Fiona is rough.[CWA. Example of deepest failure = (rule7 <- rule9 <- rule8 <- FAIL)]]
("Fiona" "is" "rough" "-")
Erin is cold.
Unknown
rconc
[@3: Erin is cold.[CWA. Example of deepest failure = (rule8 <- rule7 <- rule1 <- FAIL)]]
("Erin" "is" "cold" "+")
Erin is not rough.
Unknown
inv-rconc
[@3: Erin is rough.[CWA. Example of deepest failure = (rule7 <- rule9 <- rule8 <- FAIL)]]
("Erin" "is" "rough" "-")
Fiona is round.
Unknown
rconc
[@4: Fiona is round.[CWA. Example of deepest failure = (rule1 <- rule7 <- rule9 <- rule8 <- FAIL)]]
("Fiona" "is" "round" "+")
Dave is not green.
Unknown
inv-random
[@0: Dave is green.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "green" "-")
Erin is green.
Unknown
random
[@0: Erin is green.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "green" "+")
@0: Anne is big.[(triple1 OR ((triple2 ((((triple4) -> rule3)) -> rule2)) -> rule4) OR ((triple2 ((((triple3 triple2) -> rule6)) -> rule2)) -> rule4) OR ((((((triple4) -> rule7)) -> rule8) ((((triple4) -> rule3)) -> rule2)) -> rule4) OR ((((((triple4) -> rule7)) -> rule8) ((((triple3 triple2) -> rule6)) -> rule2)) -> rule4) OR ((triple2 ((((((triple2) -> rule9)) -> rule3)) -> rule2)) -> rule4) OR ((((((triple4) -> rule7)) -> rule8) ((((((triple2) -> rule9)) -> rule3)) -> rule2)) -> rule4) OR ((triple2 ((((triple3 ((((triple4) -> rule7)) -> rule8)) -> rule6)) -> rule2)) -> rule4) OR ((((((triple4) -> rule7)) -> rule8) ((((triple3 ((((triple4) -> rule7)) -> rule8)) -> rule6)) -> rule2)) -> rule4))] Anne is cold.[(triple2 OR ((((triple4) -> rule7)) -> rule8))] Anne is green.[(triple3)] Anne is round.[(triple4 OR ((triple2) -> rule9))] Dave is rough.[(triple5)] Erin is big.[(triple6)] Erin is furry.[(triple7)] Erin is white.[(triple8 OR ((triple7) -> rule2))] Fiona is big.[(triple9)] Fiona is furry.[(triple10)] @1: Anne is furry.[(((triple4) -> rule3) OR ((triple3 triple2) -> rule6) OR ((((triple2) -> rule9)) -> rule3) OR ((triple3 ((((triple4) -> rule7)) -> rule8)) -> rule6))] Anne is rough.[(((triple4) -> rule7) OR ((((triple2) -> rule9)) -> rule7))] Dave is cold.[(((triple5) -> rule8))] Fiona is white.[(((triple10) -> rule2))] @2: Anne is white.[(((((triple4) -> rule3)) -> rule2) OR ((((triple3 triple2) -> rule6)) -> rule2) OR ((((((triple2) -> rule9)) -> rule3)) -> rule2) OR ((((triple3 ((((triple4) -> rule7)) -> rule8)) -> rule6)) -> rule2))] Dave is round.[(((((triple5) -> rule8)) -> rule9))] @3: Dave is furry.[(((((((triple5) -> rule8)) -> rule9)) -> rule3))] @4: Dave is white.[(((((((((triple5) -> rule8)) -> rule9)) -> rule3)) -> rule2))] @5: Dave is big.[(((((triple5) -> rule8) ((((((((triple5) -> rule8)) -> rule9)) -> rule3)) -> rule2)) -> rule4))]
Anne is big.
("Anne" "is" "big" "+")
triple1
((triple2 ((((triple4) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
((triple2 ((((triple3 triple2) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
((((((triple4) -> (rule7 % int5))) -> (rule8 % int4)) ((((triple4) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Anne is cold.
("Anne" "is" "cold" "+")
int4
Anne is rough.
("Anne" "is" "rough" "+")
int5
((((((triple4) -> (rule7 % int5))) -> (rule8 % int4)) ((((triple3 triple2) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Anne is cold.
("Anne" "is" "cold" "+")
int4
Anne is rough.
("Anne" "is" "rough" "+")
int5
((triple2 ((((((triple2) -> (rule9 % int4))) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Anne is round.
("Anne" "is" "round" "+")
int4
((((((triple4) -> (rule7 % int6))) -> (rule8 % int5)) ((((((triple2) -> (rule9 % int4))) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Anne is round.
("Anne" "is" "round" "+")
int4
Anne is cold.
("Anne" "is" "cold" "+")
int5
Anne is rough.
("Anne" "is" "rough" "+")
int6
((triple2 ((((triple3 ((((triple4) -> (rule7 % int5))) -> (rule8 % int4))) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Anne is cold.
("Anne" "is" "cold" "+")
int4
Anne is rough.
("Anne" "is" "rough" "+")
int5
((((((triple4) -> (rule7 % int5))) -> (rule8 % int4)) ((((triple3 ((((triple4) -> (rule7 % int5))) -> (rule8 % int4))) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Anne is cold.
("Anne" "is" "cold" "+")
int4
Anne is rough.
("Anne" "is" "rough" "+")
int5
Anne is cold.
("Anne" "is" "cold" "+")
triple2
((((triple4) -> (rule7 % int2))) -> (rule8 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
triple3
Anne is round.
("Anne" "is" "round" "+")
triple4
((triple2) -> (rule9 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
triple5
Erin is big.
("Erin" "is" "big" "+")
triple6
Erin is furry.
("Erin" "is" "furry" "+")
triple7
Erin is white.
("Erin" "is" "white" "+")
triple8
((triple7) -> (rule2 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
triple9
Fiona is furry.
("Fiona" "is" "furry" "+")
triple10
Anne is furry.
("Anne" "is" "furry" "+")
((triple4) -> (rule3 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
((triple3 triple2) -> (rule6 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
((((triple2) -> (rule9 % int2))) -> (rule3 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
((triple3 ((((triple4) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
Anne is rough.
("Anne" "is" "rough" "+")
((triple4) -> (rule7 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
((((triple2) -> (rule9 % int2))) -> (rule7 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
((triple5) -> (rule8 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
((triple10) -> (rule2 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
((((triple4) -> (rule3 % int2))) -> (rule2 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
((((triple3 triple2) -> (rule6 % int2))) -> (rule2 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
((((((triple2) -> (rule9 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
((((triple3 ((((triple4) -> (rule7 % int4))) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Anne is rough.
("Anne" "is" "rough" "+")
int4
Dave is round.
("Dave" "is" "round" "+")
((((triple5) -> (rule8 % int2))) -> (rule9 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
((((((triple5) -> (rule8 % int3))) -> (rule9 % int2))) -> (rule3 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
((((((((triple5) -> (rule8 % int4))) -> (rule9 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is cold.
("Dave" "is" "cold" "+")
int4
Dave is big.
("Dave" "is" "big" "+")
((((triple5) -> (rule8 % int5)) ((((((((triple5) -> (rule8 % int5))) -> (rule9 % int4))) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Dave is round.
("Dave" "is" "round" "+")
int4
Dave is cold.
("Dave" "is" "cold" "+")
int5