Anne is quiet. Fiona is not green. If Anne is quiet and Anne is green then Anne is not red. If Fiona is not nice then Fiona is round. All white things are not round. If something is white then it is green. If Fiona is nice and Fiona is quiet then Fiona is blue. Quiet things are white.
Anne is quiet.
("Anne" "is" "quiet" "+")
Fiona is not green.
("Fiona" "is" "green" "-")
If Anne is quiet and Anne is green then Anne is not red.
((("Anne" "is" "quiet" "+") ("Anne" "is" "green" "+")) -> ("Anne" "is" "red" "-"))
If Fiona is not nice then Fiona is round.
((("Fiona" "is" "nice" "~")) -> ("Fiona" "is" "round" "+"))
All white things are not round.
((("something" "is" "white" "+")) -> ("something" "is" "round" "-"))
If something is white then it is green.
((("something" "is" "white" "+")) -> ("something" "is" "green" "+"))
If Fiona is nice and Fiona is quiet then Fiona is blue.
((("Fiona" "is" "nice" "+") ("Fiona" "is" "quiet" "+")) -> ("Fiona" "is" "blue" "+"))
Quiet things are white.
((("something" "is" "quiet" "+")) -> ("something" "is" "white" "+"))
Anne is quiet.
True
1
proof
[(triple1)]
("Anne" "is" "quiet" "+")
triple1
Fiona is green.
False
1
inv-proof
[(triple2)]
("Fiona" "is" "green" "+")
triple2
Anne is white.
True
2
proof
[(((triple1) -> rule6))]
("Anne" "is" "white" "+")
((triple1) -> (rule6 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is not white.
False
2
inv-proof
[(((triple1) -> rule6))]
("Anne" "is" "white" "-")
((triple1) -> (rule6 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is not round.
True
3
proof
[(((((triple1) -> rule6)) -> rule3))]
("Anne" "is" "round" "-")
((((triple1) -> (rule6 % int2))) -> (rule3 % int1))
Anne is not round.
("Anne" "is" "round" "-")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is not green.
False
3
inv-proof
[(((((triple1) -> rule6)) -> rule4))]
("Anne" "is" "green" "-")
((((triple1) -> (rule6 % int2))) -> (rule4 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is not red.
True
5
proof
[(((triple1 ((((triple1) -> rule6)) -> rule4)) -> rule1))]
("Anne" "is" "red" "-")
((triple1 ((((triple1) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Anne is not red.
("Anne" "is" "red" "-")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
Anne is red.
False
5
inv-proof
[(((triple1 ((((triple1) -> rule6)) -> rule4)) -> rule1))]
("Anne" "is" "red" "+")
((triple1 ((((triple1) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Anne is not red.
("Anne" "is" "red" "-")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
Fiona is not blue.
Unknown
inv-rconc
[@1: Fiona is blue.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Fiona" "is" "blue" "-")
Fiona is white.
Unknown
rconc
[@1: Fiona is white.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Fiona" "is" "white" "+")
Fiona is not round.
Unknown
inv-rconc
[@1: Fiona is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Fiona" "is" "round" "-")
Fiona is quiet.
Unknown
random
[@0: Fiona is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "quiet" "+")
Anne is not blue.
Unknown
inv-random
[@0: Anne is blue.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "blue" "-")
Anne is nice.
Unknown
random
[@0: Anne is nice.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "nice" "+")
Fiona is not red.
Unknown
inv-random
[@0: Fiona is red.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "red" "-")
Fiona is nice.
Unknown
random
[@0: Fiona is nice.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "nice" "+")
@0: Anne is quiet.[(triple1)] Fiona is not green.[(triple2)] @1: Anne is white.[(((triple1) -> rule6))] @2: Anne is green.[(((((triple1) -> rule6)) -> rule4))] Anne is not round.[(((((triple1) -> rule6)) -> rule3))] @3: Anne is not red.[(((triple1 ((((triple1) -> rule6)) -> rule4)) -> rule1))]
Anne is quiet.
("Anne" "is" "quiet" "+")
triple1
Fiona is not green.
("Fiona" "is" "green" "-")
triple2
Anne is white.
("Anne" "is" "white" "+")
((triple1) -> (rule6 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
((((triple1) -> (rule6 % int2))) -> (rule4 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is not round.
("Anne" "is" "round" "-")
((((triple1) -> (rule6 % int2))) -> (rule3 % int1))
Anne is not round.
("Anne" "is" "round" "-")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is not red.
("Anne" "is" "red" "-")
((triple1 ((((triple1) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Anne is not red.
("Anne" "is" "red" "-")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3