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