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