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