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