Anne is nice. Dave is red. Fiona is red. If Fiona is nice and Fiona is blue then Fiona is red. If Anne is cold and Anne is red then Anne is nice. If someone is red then they are green. Round people are not nice. If someone is red and green then they are round. Rough people are red. If Anne is red and Anne is round then Anne is not green. If Fiona is not cold then Fiona is blue.
Anne is nice.
("Anne" "is" "nice" "+")
Dave is red.
("Dave" "is" "red" "+")
Fiona is red.
("Fiona" "is" "red" "+")
If Fiona is nice and Fiona is blue then Fiona is red.
((("Fiona" "is" "nice" "+") ("Fiona" "is" "blue" "+")) -> ("Fiona" "is" "red" "+"))
If Anne is cold and Anne is red then Anne is nice.
((("Anne" "is" "cold" "+") ("Anne" "is" "red" "+")) -> ("Anne" "is" "nice" "+"))
If someone is red then they are green.
((("someone" "is" "red" "+")) -> ("someone" "is" "green" "+"))
Round people are not nice.
((("someone" "is" "round" "+")) -> ("someone" "is" "nice" "-"))
If someone is red and green then they are round.
((("someone" "is" "red" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "round" "+"))
Rough people are red.
((("someone" "is" "rough" "+")) -> ("someone" "is" "red" "+"))
If Anne is red and Anne is round then Anne is not green.
((("Anne" "is" "red" "+") ("Anne" "is" "round" "+")) -> ("Anne" "is" "green" "-"))
If Fiona is not cold then Fiona is blue.
((("Fiona" "is" "cold" "~")) -> ("Fiona" "is" "blue" "+"))
Dave is red.
True
1
proof
[(triple2)]
("Dave" "is" "red" "+")
triple2
Anne is not nice.
False
1
inv-proof
[(triple1)]
("Anne" "is" "nice" "-")
triple1
Dave is green.
True
2
proof
[(((triple2) -> rule3))]
("Dave" "is" "green" "+")
((triple2) -> (rule3 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is not green.
False
2
inv-proof
[(((triple2) -> rule3))]
("Dave" "is" "green" "-")
((triple2) -> (rule3 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Fiona is round.
True
4
proof
[(((triple3 ((triple3) -> rule3)) -> rule5))]
("Fiona" "is" "round" "+")
((triple3 ((triple3) -> (rule3 % int2))) -> (rule5 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Dave is not round.
False
4
inv-proof
[(((triple2 ((triple2) -> rule3)) -> rule5))]
("Dave" "is" "round" "-")
((triple2 ((triple2) -> (rule3 % int2))) -> (rule5 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is not nice.
True
5
proof
[(((((triple2 ((triple2) -> rule3)) -> rule5)) -> rule4))]
("Dave" "is" "nice" "-")
((((triple2 ((triple2) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Dave is not nice.
("Dave" "is" "nice" "-")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Fiona is nice.
False
5
inv-proof
[(((((triple3 ((triple3) -> rule3)) -> rule5)) -> rule4))]
("Fiona" "is" "nice" "+")
((((triple3 ((triple3) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Fiona is not nice.
("Fiona" "is" "nice" "-")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
int3
Anne is not red.
Unknown
inv-rconc
[@1: Anne is red.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Anne" "is" "red" "-")
Anne is green.
Unknown
rconc
[@2: Anne is green.[CWA. Example of deepest failure = (rule3 <- rule6 <- FAIL)]]
("Anne" "is" "green" "+")
Fiona is not blue.
Unknown
inv-rconc
[@1: Fiona is blue.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Fiona" "is" "blue" "-")
Anne is round.
Unknown
rconc
[@2: Anne is round.[CWA. Example of deepest failure = (rule5 <- rule6 <- FAIL)]]
("Anne" "is" "round" "+")
Anne is not blue.
Unknown
inv-random
[@0: Anne is blue.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "blue" "-")
Anne is cold.
Unknown
random
[@0: Anne is cold.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "cold" "+")
Dave is not rough.
Unknown
inv-random
[@0: Dave is rough.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "rough" "-")
Dave is blue.
Unknown
random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "+")
@0: Anne is nice.[(triple1)] Dave is red.[(triple2)] Fiona is red.[(triple3)] @1: Dave is green.[(((triple2) -> rule3))] Fiona is green.[(((triple3) -> rule3))] @2: Dave is round.[(((triple2 ((triple2) -> rule3)) -> rule5))] Fiona is round.[(((triple3 ((triple3) -> rule3)) -> rule5))] @3: Dave is not nice.[(((((triple2 ((triple2) -> rule3)) -> rule5)) -> rule4))] Fiona is not nice.[(((((triple3 ((triple3) -> rule3)) -> rule5)) -> rule4))]
Anne is nice.
("Anne" "is" "nice" "+")
triple1
Dave is red.
("Dave" "is" "red" "+")
triple2
Fiona is red.
("Fiona" "is" "red" "+")
triple3
Dave is green.
("Dave" "is" "green" "+")
((triple2) -> (rule3 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
((triple3) -> (rule3 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
((triple2 ((triple2) -> (rule3 % int2))) -> (rule5 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
((triple3 ((triple3) -> (rule3 % int2))) -> (rule5 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Dave is not nice.
("Dave" "is" "nice" "-")
((((triple2 ((triple2) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Dave is not nice.
("Dave" "is" "nice" "-")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Fiona is not nice.
("Fiona" "is" "nice" "-")
((((triple3 ((triple3) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Fiona is not nice.
("Fiona" "is" "nice" "-")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
int3