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