Anne is big. Anne is cold. Bob is big. Bob is blue. Bob is cold. Bob is round. Charlie is furry. Charlie is round. Charlie is white. Erin is big. Erin is red. Erin is white. If someone is round then they are furry. White, blue people are red. All big, round people are red. Red people are white. If someone is red then they are furry. If Anne is blue then Anne is white. All furry people are round. All big people are blue. Red, blue people are big.
Anne is big.
("Anne" "is" "big" "+")
Anne is cold.
("Anne" "is" "cold" "+")
Bob is big.
("Bob" "is" "big" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is round.
("Bob" "is" "round" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is white.
("Erin" "is" "white" "+")
If someone is round then they are furry.
((("someone" "is" "round" "+")) -> ("someone" "is" "furry" "+"))
White, blue people are red.
((("someone" "is" "white" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "red" "+"))
All big, round people are red.
((("someone" "is" "big" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "red" "+"))
Red people are white.
((("someone" "is" "red" "+")) -> ("someone" "is" "white" "+"))
If someone is red then they are furry.
((("someone" "is" "red" "+")) -> ("someone" "is" "furry" "+"))
If Anne is blue then Anne is white.
((("Anne" "is" "blue" "+")) -> ("Anne" "is" "white" "+"))
All furry people are round.
((("someone" "is" "furry" "+")) -> ("someone" "is" "round" "+"))
All big people are blue.
((("someone" "is" "big" "+")) -> ("someone" "is" "blue" "+"))
Red, blue people are big.
((("someone" "is" "red" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "big" "+"))
Erin is big.
True
1
proof
[(triple10)]
("Erin" "is" "big" "+")
triple10
Bob is not big.
False
1
inv-proof
[(triple3)]
("Bob" "is" "big" "-")
triple3
Bob is furry.
True
2
proof
[(((triple6) -> rule1) OR ((((triple3 triple6) -> rule3)) -> rule5))]
("Bob" "is" "furry" "+")
((triple6) -> (rule1 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
((((triple3 triple6) -> (rule3 % int2))) -> (rule5 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Anne is not blue.
False
2
inv-proof
[(((triple1) -> rule8))]
("Anne" "is" "blue" "-")
((triple1) -> (rule8 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Bob is white.
True
4
proof
[(((((triple3 triple6) -> rule3)) -> rule4))]
("Bob" "is" "white" "+")
((((triple3 triple6) -> (rule3 % int2))) -> (rule4 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Erin is not round.
False
3
inv-proof
[(((((triple11) -> rule5)) -> rule7) OR ((((((triple12 ((triple10) -> rule8)) -> rule2)) -> rule5)) -> rule7))]
("Erin" "is" "round" "-")
((((triple11) -> (rule5 % int2))) -> (rule7 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
((((((triple12 ((triple10) -> (rule8 % int4))) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
Erin is blue.
("Erin" "is" "blue" "+")
int4
Anne is red.
True
6
proof
[(((((((triple1) -> rule8)) -> rule6) ((triple1) -> rule8)) -> rule2))]
("Anne" "is" "red" "+")
((((((triple1) -> (rule8 % int3))) -> (rule6 % int2)) ((triple1) -> (rule8 % int3))) -> (rule2 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
Anne is not red.
False
6
inv-proof
[(((((((triple1) -> rule8)) -> rule6) ((triple1) -> rule8)) -> rule2))]
("Anne" "is" "red" "-")
((((((triple1) -> (rule8 % int3))) -> (rule6 % int2)) ((triple1) -> (rule8 % int3))) -> (rule2 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
Anne is furry.
True
7
proof
[(((((((((triple1) -> rule8)) -> rule6) ((triple1) -> rule8)) -> rule2)) -> rule5))]
("Anne" "is" "furry" "+")
((((((((triple1) -> (rule8 % int4))) -> (rule6 % int3)) ((triple1) -> (rule8 % int4))) -> (rule2 % int2))) -> (rule5 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
Anne is blue.
("Anne" "is" "blue" "+")
int4
Anne is not furry.
False
7
inv-proof
[(((((((((triple1) -> rule8)) -> rule6) ((triple1) -> rule8)) -> rule2)) -> rule5))]
("Anne" "is" "furry" "-")
((((((((triple1) -> (rule8 % int4))) -> (rule6 % int3)) ((triple1) -> (rule8 % int4))) -> (rule2 % int2))) -> (rule5 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
Anne is blue.
("Anne" "is" "blue" "+")
int4
Anne is round.
True
8
proof
[(((((((((((triple1) -> rule8)) -> rule6) ((triple1) -> rule8)) -> rule2)) -> rule5)) -> rule7))]
("Anne" "is" "round" "+")
((((((((((triple1) -> (rule8 % int5))) -> (rule6 % int4)) ((triple1) -> (rule8 % int5))) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Anne is white.
("Anne" "is" "white" "+")
int4
Anne is blue.
("Anne" "is" "blue" "+")
int5
Anne is not round.
False
8
inv-proof
[(((((((((((triple1) -> rule8)) -> rule6) ((triple1) -> rule8)) -> rule2)) -> rule5)) -> rule7))]
("Anne" "is" "round" "-")
((((((((((triple1) -> (rule8 % int5))) -> (rule6 % int4)) ((triple1) -> (rule8 % int5))) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Anne is white.
("Anne" "is" "white" "+")
int4
Anne is blue.
("Anne" "is" "blue" "+")
int5
Charlie is not big.
Unknown
inv-rconc
[@2: Charlie is big.[CWA. Example of deepest failure = (rule9 <- rule8 <- FAIL)]]
("Charlie" "is" "big" "-")
Charlie is blue.
Unknown
rconc
[@2: Charlie is blue.[CWA. Example of deepest failure = (rule8 <- rule9 <- FAIL)]]
("Charlie" "is" "blue" "+")
Charlie is not red.
Unknown
inv-rconc
[@3: Charlie is red.[CWA. Example of deepest failure = (rule2 <- rule8 <- rule9 <- FAIL)]]
("Charlie" "is" "red" "-")
Erin is cold.
Unknown
random
[@0: Erin is cold.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "cold" "+")
@0: Anne is big.[(triple1)] Anne is cold.[(triple2)] Bob is big.[(triple3)] Bob is blue.[(triple4 OR ((triple3) -> rule8))] Bob is cold.[(triple5)] Bob is round.[(triple6)] Charlie is furry.[(triple7 OR ((triple8) -> rule1))] Charlie is round.[(triple8 OR ((triple7) -> rule7))] Charlie is white.[(triple9)] Erin is big.[(triple10)] Erin is red.[(triple11 OR ((triple12 ((triple10) -> rule8)) -> rule2))] Erin is white.[(triple12 OR ((triple11) -> rule4))] @1: Anne is blue.[(((triple1) -> rule8))] Bob is furry.[(((triple6) -> rule1) OR ((((triple3 triple6) -> rule3)) -> rule5))] Bob is red.[(((triple3 triple6) -> rule3))] Erin is blue.[(((triple10) -> rule8))] Erin is furry.[(((triple11) -> rule5) OR ((((triple12 ((triple10) -> rule8)) -> rule2)) -> rule5))] @2: Anne is white.[(((((triple1) -> rule8)) -> rule6))] Bob is white.[(((((triple3 triple6) -> rule3)) -> rule4))] Erin is round.[(((((triple11) -> rule5)) -> rule7) OR ((((((triple12 ((triple10) -> rule8)) -> rule2)) -> rule5)) -> rule7))] @3: Anne is red.[(((((((triple1) -> rule8)) -> rule6) ((triple1) -> rule8)) -> rule2))] @4: Anne is furry.[(((((((((triple1) -> rule8)) -> rule6) ((triple1) -> rule8)) -> rule2)) -> rule5))] @5: Anne is round.[(((((((((((triple1) -> rule8)) -> rule6) ((triple1) -> rule8)) -> rule2)) -> rule5)) -> rule7))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is cold.
("Anne" "is" "cold" "+")
triple2
Bob is big.
("Bob" "is" "big" "+")
triple3
Bob is blue.
("Bob" "is" "blue" "+")
triple4
((triple3) -> (rule8 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
triple5
Bob is round.
("Bob" "is" "round" "+")
triple6
Charlie is furry.
("Charlie" "is" "furry" "+")
triple7
((triple8) -> (rule1 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
triple8
((triple7) -> (rule7 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
triple9
Erin is big.
("Erin" "is" "big" "+")
triple10
Erin is red.
("Erin" "is" "red" "+")
triple11
((triple12 ((triple10) -> (rule8 % int2))) -> (rule2 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
triple12
((triple11) -> (rule4 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
((triple1) -> (rule8 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
((triple6) -> (rule1 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
((((triple3 triple6) -> (rule3 % int2))) -> (rule5 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
((triple3 triple6) -> (rule3 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
((triple10) -> (rule8 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
((triple11) -> (rule5 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
((((triple12 ((triple10) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
Anne is white.
("Anne" "is" "white" "+")
((((triple1) -> (rule8 % int2))) -> (rule6 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
((((triple3 triple6) -> (rule3 % int2))) -> (rule4 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
((((triple11) -> (rule5 % int2))) -> (rule7 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
((((((triple12 ((triple10) -> (rule8 % int4))) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
Erin is blue.
("Erin" "is" "blue" "+")
int4
Anne is red.
("Anne" "is" "red" "+")
((((((triple1) -> (rule8 % int3))) -> (rule6 % int2)) ((triple1) -> (rule8 % int3))) -> (rule2 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
Anne is furry.
("Anne" "is" "furry" "+")
((((((((triple1) -> (rule8 % int4))) -> (rule6 % int3)) ((triple1) -> (rule8 % int4))) -> (rule2 % int2))) -> (rule5 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
Anne is blue.
("Anne" "is" "blue" "+")
int4
Anne is round.
("Anne" "is" "round" "+")
((((((((((triple1) -> (rule8 % int5))) -> (rule6 % int4)) ((triple1) -> (rule8 % int5))) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Anne is white.
("Anne" "is" "white" "+")
int4
Anne is blue.
("Anne" "is" "blue" "+")
int5