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