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