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