Anne is not kind. Anne is rough. Charlie is round. If something is nice then it is green. Rough things are big. If something is big then it is nice. Green, big things are red. If Anne is not big then Anne is green. If something is round and not red then it is kind.
Anne is not kind.
("Anne" "is" "kind" "-")
Anne is rough.
("Anne" "is" "rough" "+")
Charlie is round.
("Charlie" "is" "round" "+")
If something is nice then it is green.
((("something" "is" "nice" "+")) -> ("something" "is" "green" "+"))
Rough things are big.
((("something" "is" "rough" "+")) -> ("something" "is" "big" "+"))
If something is big then it is nice.
((("something" "is" "big" "+")) -> ("something" "is" "nice" "+"))
Green, big things are red.
((("something" "is" "green" "+") ("something" "is" "big" "+")) -> ("something" "is" "red" "+"))
If Anne is not big then Anne is green.
((("Anne" "is" "big" "~")) -> ("Anne" "is" "green" "+"))
If something is round and not red then it is kind.
((("something" "is" "round" "+") ("something" "is" "red" "~")) -> ("something" "is" "kind" "+"))
Anne is rough.
True
1
proof
[(triple2)]
("Anne" "is" "rough" "+")
triple2
Anne is not rough.
False
1
inv-proof
[(triple2)]
("Anne" "is" "rough" "-")
triple2
Anne is big.
True
2
proof
[(((triple2) -> rule2))]
("Anne" "is" "big" "+")
((triple2) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is not big.
False
2
inv-proof
[(((triple2) -> rule2))]
("Anne" "is" "big" "-")
((triple2) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is nice.
True
3
proof
[(((((triple2) -> rule2)) -> rule3))]
("Anne" "is" "nice" "+")
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is not nice.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule3))]
("Anne" "is" "nice" "-")
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is green.
True
4
proof
[(((((((triple2) -> rule2)) -> rule3)) -> rule1))]
("Anne" "is" "green" "+")
((((((triple2) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
Anne is not green.
False
4
inv-proof
[(((((((triple2) -> rule2)) -> rule3)) -> rule1))]
("Anne" "is" "green" "-")
((((((triple2) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
Charlie is not kind.
Unknown
inv-rconc
[@1: Charlie is kind.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Charlie" "is" "kind" "-")
Charlie is red.
Unknown
rconc
[@2: Charlie is red.[CWA. Example of deepest failure = (rule4 <- rule2 <- FAIL)]]
("Charlie" "is" "red" "+")
Charlie is not green.
Unknown
inv-rconc
[@3: Charlie is green.[CWA. Example of deepest failure = (rule1 <- rule3 <- rule2 <- FAIL)]]
("Charlie" "is" "green" "-")
Charlie is big.
Unknown
rconc
[@1: Charlie is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "big" "+")
Charlie is not rough.
Unknown
inv-random
[@0: Charlie is rough.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "rough" "-")
Anne is round.
Unknown
random
[@0: Anne is round.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "round" "+")
@0: Anne is not kind.[(triple1)] Anne is rough.[(triple2)] Charlie is round.[(triple3)] @1: Anne is big.[(((triple2) -> rule2))] @2: Anne is nice.[(((((triple2) -> rule2)) -> rule3))] @3: Anne is green.[(((((((triple2) -> rule2)) -> rule3)) -> rule1))] @4: Anne is red.[(((((((((triple2) -> rule2)) -> rule3)) -> rule1) ((triple2) -> rule2)) -> rule4))]
Anne is not kind.
("Anne" "is" "kind" "-")
triple1
Anne is rough.
("Anne" "is" "rough" "+")
triple2
Charlie is round.
("Charlie" "is" "round" "+")
triple3
Anne is big.
("Anne" "is" "big" "+")
((triple2) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
((((((triple2) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
Anne is red.
("Anne" "is" "red" "+")
((((((((triple2) -> (rule2 % int4))) -> (rule3 % int3))) -> (rule1 % int2)) ((triple2) -> (rule2 % int4))) -> (rule4 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Anne is big.
("Anne" "is" "big" "+")
int4