Anne is white. Erin is big. Fiona is green. Gary is young. White things are big. If something is big then it is green. All green things are red. If something is green and cold then it is big. If Gary is white and Gary is red then Gary is round. If Anne is white then Anne is big.
Anne is white.
("Anne" "is" "white" "+")
Erin is big.
("Erin" "is" "big" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Gary is young.
("Gary" "is" "young" "+")
White things are big.
((("something" "is" "white" "+")) -> ("something" "is" "big" "+"))
If something is big then it is green.
((("something" "is" "big" "+")) -> ("something" "is" "green" "+"))
All green things are red.
((("something" "is" "green" "+")) -> ("something" "is" "red" "+"))
If something is green and cold then it is big.
((("something" "is" "green" "+") ("something" "is" "cold" "+")) -> ("something" "is" "big" "+"))
If Gary is white and Gary is red then Gary is round.
((("Gary" "is" "white" "+") ("Gary" "is" "red" "+")) -> ("Gary" "is" "round" "+"))
If Anne is white then Anne is big.
((("Anne" "is" "white" "+")) -> ("Anne" "is" "big" "+"))
Erin is big.
True
1
proof
[(triple2)]
("Erin" "is" "big" "+")
triple2
Anne is not white.
False
1
inv-proof
[(triple1)]
("Anne" "is" "white" "-")
triple1
Fiona is red.
True
2
proof
[(((triple3) -> rule3))]
("Fiona" "is" "red" "+")
((triple3) -> (rule3 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Erin is not green.
False
2
inv-proof
[(((triple2) -> rule2))]
("Erin" "is" "green" "-")
((triple2) -> (rule2 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is red.
True
3
proof
[(((((triple2) -> rule2)) -> rule3))]
("Erin" "is" "red" "+")
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Anne is not green.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule2) OR ((((triple1) -> rule6)) -> rule2))]
("Anne" "is" "green" "-")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
((((triple1) -> (rule6 % int2))) -> (rule2 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is red.
True
4
proof
[(((((((triple1) -> rule1)) -> rule2)) -> rule3) OR ((((((triple1) -> rule6)) -> rule2)) -> rule3))]
("Anne" "is" "red" "+")
((((((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
((((((triple1) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
Anne is not red.
False
4
inv-proof
[(((((((triple1) -> rule1)) -> rule2)) -> rule3) OR ((((((triple1) -> rule6)) -> rule2)) -> rule3))]
("Anne" "is" "red" "-")
((((((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
((((((triple1) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
Gary is not green.
Unknown
inv-rconc
[@2: Gary is green.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("Gary" "is" "green" "-")
Gary is red.
Unknown
rconc
[@3: Gary is red.[CWA. Example of deepest failure = (rule3 <- rule2 <- rule1 <- FAIL)]]
("Gary" "is" "red" "+")
Fiona is not big.
Unknown
inv-rconc
[@1: Fiona is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "big" "-")
Gary is round.
Unknown
rconc
[@1: Gary is round.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Gary" "is" "round" "+")
Erin is not cold.
Unknown
inv-random
[@0: Erin is cold.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "cold" "-")
Erin is white.
Unknown
random
[@0: Erin is white.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "white" "+")
Fiona is not young.
Unknown
inv-random
[@0: Fiona is young.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "young" "-")
Fiona is cold.
Unknown
random
[@0: Fiona is cold.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "cold" "+")
@0: Anne is white.[(triple1)] Erin is big.[(triple2)] Fiona is green.[(triple3)] Gary is young.[(triple4)] @1: Anne is big.[(((triple1) -> rule1) OR ((triple1) -> rule6))] Erin is green.[(((triple2) -> rule2))] Fiona is red.[(((triple3) -> rule3))] @2: Anne is green.[(((((triple1) -> rule1)) -> rule2) OR ((((triple1) -> rule6)) -> rule2))] Erin is red.[(((((triple2) -> rule2)) -> rule3))] @3: Anne is red.[(((((((triple1) -> rule1)) -> rule2)) -> rule3) OR ((((((triple1) -> rule6)) -> rule2)) -> rule3))]
Anne is white.
("Anne" "is" "white" "+")
triple1
Erin is big.
("Erin" "is" "big" "+")
triple2
Fiona is green.
("Fiona" "is" "green" "+")
triple3
Gary is young.
("Gary" "is" "young" "+")
triple4
Anne is big.
("Anne" "is" "big" "+")
((triple1) -> (rule1 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
((triple1) -> (rule6 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
((triple2) -> (rule2 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
((triple3) -> (rule3 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
((((triple1) -> (rule6 % int2))) -> (rule2 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
((((((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
((((((triple1) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3