Anne is blue. Dave is green. Fiona is cold. Gary is white. If Gary is green and Gary is big then Gary is blue. If someone is green then they are big. If someone is rough and green then they are not big. If someone is green then they are round. White people are green. If Gary is rough and Gary is not big then Gary is not cold.
Anne is blue.
("Anne" "is" "blue" "+")
Dave is green.
("Dave" "is" "green" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Gary is white.
("Gary" "is" "white" "+")
If Gary is green and Gary is big then Gary is blue.
((("Gary" "is" "green" "+") ("Gary" "is" "big" "+")) -> ("Gary" "is" "blue" "+"))
If someone is green then they are big.
((("someone" "is" "green" "+")) -> ("someone" "is" "big" "+"))
If someone is rough and green then they are not big.
((("someone" "is" "rough" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "big" "-"))
If someone is green then they are round.
((("someone" "is" "green" "+")) -> ("someone" "is" "round" "+"))
White people are green.
((("someone" "is" "white" "+")) -> ("someone" "is" "green" "+"))
If Gary is rough and Gary is not big then Gary is not cold.
((("Gary" "is" "rough" "+") ("Gary" "is" "big" "~")) -> ("Gary" "is" "cold" "-"))
Dave is green.
True
1
proof
[(triple2)]
("Dave" "is" "green" "+")
triple2
Anne is not blue.
False
1
inv-proof
[(triple1)]
("Anne" "is" "blue" "-")
triple1
Dave is round.
True
2
proof
[(((triple2) -> rule4))]
("Dave" "is" "round" "+")
((triple2) -> (rule4 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is not big.
False
2
inv-proof
[(((triple2) -> rule2))]
("Dave" "is" "big" "-")
((triple2) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Gary is round.
True
3
proof
[(((((triple4) -> rule5)) -> rule4))]
("Gary" "is" "round" "+")
((((triple4) -> (rule5 % int2))) -> (rule4 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is not big.
False
3
inv-proof
[(((((triple4) -> rule5)) -> rule2))]
("Gary" "is" "big" "-")
((((triple4) -> (rule5 % int2))) -> (rule2 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is blue.
True
6
proof
[(((((triple4) -> rule5) ((((triple4) -> rule5)) -> rule2)) -> rule1))]
("Gary" "is" "blue" "+")
((((triple4) -> (rule5 % int3)) ((((triple4) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
Gary is not blue.
False
6
inv-proof
[(((((triple4) -> rule5) ((((triple4) -> rule5)) -> rule2)) -> rule1))]
("Gary" "is" "blue" "-")
((((triple4) -> (rule5 % int3)) ((((triple4) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
Anne is not big.
Unknown
inv-rconc
[@2: Anne is big.[CWA. Example of deepest failure = (rule2 <- rule5 <- FAIL)]]
("Anne" "is" "big" "-")
Fiona is round.
Unknown
rconc
[@2: Fiona is round.[CWA. Example of deepest failure = (rule4 <- rule5 <- FAIL)]]
("Fiona" "is" "round" "+")
Anne is not green.
Unknown
inv-rconc
[@1: Anne is green.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Anne" "is" "green" "-")
Fiona is big.
Unknown
rconc
[@2: Fiona is big.[CWA. Example of deepest failure = (rule2 <- rule5 <- FAIL)]]
("Fiona" "is" "big" "+")
Fiona is not white.
Unknown
inv-random
[@0: Fiona is white.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "white" "-")
Fiona is rough.
Unknown
random
[@0: Fiona is rough.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "rough" "+")
Gary is not cold.
Unknown
inv-random
[@0: Gary is cold.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "cold" "-")
Dave is blue.
Unknown
random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "+")
@0: Anne is blue.[(triple1)] Dave is green.[(triple2)] Fiona is cold.[(triple3)] Gary is white.[(triple4)] @1: Dave is big.[(((triple2) -> rule2))] Dave is round.[(((triple2) -> rule4))] Gary is green.[(((triple4) -> rule5))] @2: Gary is big.[(((((triple4) -> rule5)) -> rule2))] Gary is round.[(((((triple4) -> rule5)) -> rule4))] @3: Gary is blue.[(((((triple4) -> rule5) ((((triple4) -> rule5)) -> rule2)) -> rule1))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Dave is green.
("Dave" "is" "green" "+")
triple2
Fiona is cold.
("Fiona" "is" "cold" "+")
triple3
Gary is white.
("Gary" "is" "white" "+")
triple4
Dave is big.
("Dave" "is" "big" "+")
((triple2) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
((triple2) -> (rule4 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
((triple4) -> (rule5 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
((((triple4) -> (rule5 % int2))) -> (rule2 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
((((triple4) -> (rule5 % int2))) -> (rule4 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
((((triple4) -> (rule5 % int3)) ((((triple4) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3