Anne is green. Anne is quiet. Charlie is quiet. Charlie is not white. Dave is young. Erin is green. Erin is young. If Charlie is young and Charlie is not quiet then Charlie is big. If Anne is green then Anne is big. If something is cold and quiet then it is red. All young, cold things are not big. All green, young things are not cold. Big things are young. If something is young and not red then it is not white. If something is cold then it is white.
Anne is green.
("Anne" "is" "green" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is not white.
("Charlie" "is" "white" "-")
Dave is young.
("Dave" "is" "young" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is young.
("Erin" "is" "young" "+")
If Charlie is young and Charlie is not quiet then Charlie is big.
((("Charlie" "is" "young" "+") ("Charlie" "is" "quiet" "~")) -> ("Charlie" "is" "big" "+"))
If Anne is green then Anne is big.
((("Anne" "is" "green" "+")) -> ("Anne" "is" "big" "+"))
If something is cold and quiet then it is red.
((("something" "is" "cold" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "red" "+"))
All young, cold things are not big.
((("something" "is" "young" "+") ("something" "is" "cold" "+")) -> ("something" "is" "big" "-"))
All green, young things are not cold.
((("something" "is" "green" "+") ("something" "is" "young" "+")) -> ("something" "is" "cold" "-"))
Big things are young.
((("something" "is" "big" "+")) -> ("something" "is" "young" "+"))
If something is young and not red then it is not white.
((("something" "is" "young" "+") ("something" "is" "red" "~")) -> ("something" "is" "white" "-"))
If something is cold then it is white.
((("something" "is" "cold" "+")) -> ("something" "is" "white" "+"))
Anne is quiet.
True
1
proof
[(triple2)]
("Anne" "is" "quiet" "+")
triple2
Anne is not green.
False
1
inv-proof
[(triple1)]
("Anne" "is" "green" "-")
triple1
Erin is not cold.
True
3
proof
[(((triple6 triple7) -> rule5))]
("Erin" "is" "cold" "-")
((triple6 triple7) -> (rule5 % int1))
Erin is not cold.
("Erin" "is" "cold" "-")
int1
Anne is not big.
False
2
inv-proof
[(((triple1) -> rule2))]
("Anne" "is" "big" "-")
((triple1) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is young.
True
3
proof
[(((((triple1) -> rule2)) -> rule6))]
("Anne" "is" "young" "+")
((((triple1) -> (rule2 % int2))) -> (rule6 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is not young.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule6))]
("Anne" "is" "young" "-")
((((triple1) -> (rule2 % int2))) -> (rule6 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is not cold.
True
5
proof
[(((triple1 ((((triple1) -> rule2)) -> rule6)) -> rule5))]
("Anne" "is" "cold" "-")
((triple1 ((((triple1) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Anne is not cold.
("Anne" "is" "cold" "-")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
Anne is cold.
False
5
inv-proof
[(((triple1 ((((triple1) -> rule2)) -> rule6)) -> rule5))]
("Anne" "is" "cold" "+")
((triple1 ((((triple1) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Anne is not cold.
("Anne" "is" "cold" "-")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
Erin is not white.
Unknown
inv-rconc
[@1: Erin is white.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Erin" "is" "white" "-")
Charlie is big.
Unknown
rconc
[@1: Charlie is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "big" "+")
Anne is not red.
Unknown
inv-rconc
[@1: Anne is red.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "red" "-")
Charlie is young.
Unknown
rconc
[@2: Charlie is young.[CWA. Example of deepest failure = (rule6 <- rule1 <- FAIL)]]
("Charlie" "is" "young" "+")
Dave is not green.
Unknown
inv-random
[@0: Dave is green.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "green" "-")
Charlie is cold.
Unknown
random
[@0: Charlie is cold.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "cold" "+")
Dave is not quiet.
Unknown
inv-random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "-")
Erin is quiet.
Unknown
random
[@0: Erin is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "quiet" "+")
@0: Anne is green.[(triple1)] Anne is quiet.[(triple2)] Charlie is not white.[(triple4)] Charlie is quiet.[(triple3)] Dave is young.[(triple5)] Erin is green.[(triple6)] Erin is young.[(triple7)] @1: Anne is big.[(((triple1) -> rule2))] Erin is not cold.[(((triple6 triple7) -> rule5))] @2: Anne is young.[(((((triple1) -> rule2)) -> rule6))] @3: Anne is not cold.[(((triple1 ((((triple1) -> rule2)) -> rule6)) -> rule5))]
Anne is green.
("Anne" "is" "green" "+")
triple1
Anne is quiet.
("Anne" "is" "quiet" "+")
triple2
Charlie is not white.
("Charlie" "is" "white" "-")
triple4
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple3
Dave is young.
("Dave" "is" "young" "+")
triple5
Erin is green.
("Erin" "is" "green" "+")
triple6
Erin is young.
("Erin" "is" "young" "+")
triple7
Anne is big.
("Anne" "is" "big" "+")
((triple1) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Erin is not cold.
("Erin" "is" "cold" "-")
((triple6 triple7) -> (rule5 % int1))
Erin is not cold.
("Erin" "is" "cold" "-")
int1
Anne is young.
("Anne" "is" "young" "+")
((((triple1) -> (rule2 % int2))) -> (rule6 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is not cold.
("Anne" "is" "cold" "-")
((triple1 ((((triple1) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Anne is not cold.
("Anne" "is" "cold" "-")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3