Anne is cold. Anne is kind. Charlie is kind. All kind, red people are furry. All cold, kind people are smart. All cold, smart people are green. Green people are rough. All red, kind people are cold. All kind people are cold.
Anne is cold.
("Anne" "is" "cold" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
All kind, red people are furry.
((("someone" "is" "kind" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "furry" "+"))
All cold, kind people are smart.
((("someone" "is" "cold" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "smart" "+"))
All cold, smart people are green.
((("someone" "is" "cold" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "green" "+"))
Green people are rough.
((("someone" "is" "green" "+")) -> ("someone" "is" "rough" "+"))
All red, kind people are cold.
((("someone" "is" "red" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "cold" "+"))
All kind people are cold.
((("someone" "is" "kind" "+")) -> ("someone" "is" "cold" "+"))
Anne is cold.
True
1
proof
[(triple1 OR ((triple2) -> rule6))]
("Anne" "is" "cold" "+")
triple1
((triple2) -> (rule6 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Charlie is not kind.
False
1
inv-proof
[(triple3)]
("Charlie" "is" "kind" "-")
triple3
Charlie is cold.
True
2
proof
[(((triple3) -> rule6))]
("Charlie" "is" "cold" "+")
((triple3) -> (rule6 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Anne is not smart.
False
3
inv-proof
[(((triple1 triple2) -> rule2) OR ((((triple2) -> rule6) triple2) -> rule2))]
("Anne" "is" "smart" "-")
((triple1 triple2) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
((((triple2) -> (rule6 % int2)) triple2) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is green.
True
5
proof
[(((triple1 ((triple1 triple2) -> rule2)) -> rule3) OR ((((triple2) -> rule6) ((triple1 triple2) -> rule2)) -> rule3) OR ((triple1 ((((triple2) -> rule6) triple2) -> rule2)) -> rule3) OR ((((triple2) -> rule6) ((((triple2) -> rule6) triple2) -> rule2)) -> rule3))]
("Anne" "is" "green" "+")
((triple1 ((triple1 triple2) -> (rule2 % int2))) -> (rule3 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
((((triple2) -> (rule6 % int3)) ((triple1 triple2) -> (rule2 % int2))) -> (rule3 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
((triple1 ((((triple2) -> (rule6 % int3)) triple2) -> (rule2 % int2))) -> (rule3 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
((((triple2) -> (rule6 % int3)) ((((triple2) -> (rule6 % int3)) triple2) -> (rule2 % int2))) -> (rule3 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Anne is not green.
False
5
inv-proof
[(((triple1 ((triple1 triple2) -> rule2)) -> rule3) OR ((((triple2) -> rule6) ((triple1 triple2) -> rule2)) -> rule3) OR ((triple1 ((((triple2) -> rule6) triple2) -> rule2)) -> rule3) OR ((((triple2) -> rule6) ((((triple2) -> rule6) triple2) -> rule2)) -> rule3))]
("Anne" "is" "green" "-")
((triple1 ((triple1 triple2) -> (rule2 % int2))) -> (rule3 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
((((triple2) -> (rule6 % int3)) ((triple1 triple2) -> (rule2 % int2))) -> (rule3 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
((triple1 ((((triple2) -> (rule6 % int3)) triple2) -> (rule2 % int2))) -> (rule3 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
((((triple2) -> (rule6 % int3)) ((((triple2) -> (rule6 % int3)) triple2) -> (rule2 % int2))) -> (rule3 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Charlie is green.
True
7
proof
[(((((triple3) -> rule6) ((((triple3) -> rule6) triple3) -> rule2)) -> rule3))]
("Charlie" "is" "green" "+")
((((triple3) -> (rule6 % int3)) ((((triple3) -> (rule6 % int3)) triple3) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
Anne is not rough.
False
6
inv-proof
[(((((triple1 ((triple1 triple2) -> rule2)) -> rule3)) -> rule4) OR ((((((triple2) -> rule6) ((triple1 triple2) -> rule2)) -> rule3)) -> rule4) OR ((((triple1 ((((triple2) -> rule6) triple2) -> rule2)) -> rule3)) -> rule4) OR ((((((triple2) -> rule6) ((((triple2) -> rule6) triple2) -> rule2)) -> rule3)) -> rule4))]
("Anne" "is" "rough" "-")
((((triple1 ((triple1 triple2) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
((((((triple2) -> (rule6 % int4)) ((triple1 triple2) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is cold.
("Anne" "is" "cold" "+")
int4
((((triple1 ((((triple2) -> (rule6 % int4)) triple2) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is cold.
("Anne" "is" "cold" "+")
int4
((((((triple2) -> (rule6 % int4)) ((((triple2) -> (rule6 % int4)) triple2) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is cold.
("Anne" "is" "cold" "+")
int4
Charlie is not furry.
Unknown
inv-rconc
[@1: Charlie is furry.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "furry" "-")
Anne is furry.
Unknown
rconc
[@1: Anne is furry.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "furry" "+")
Charlie is not red.
Unknown
inv-random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "-")
Anne is red.
Unknown
random
[@0: Anne is red.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "red" "+")
@0: Anne is cold.[(triple1 OR ((triple2) -> rule6))] Anne is kind.[(triple2)] Charlie is kind.[(triple3)] @1: Anne is smart.[(((triple1 triple2) -> rule2) OR ((((triple2) -> rule6) triple2) -> rule2))] Charlie is cold.[(((triple3) -> rule6))] @2: Anne is green.[(((triple1 ((triple1 triple2) -> rule2)) -> rule3) OR ((((triple2) -> rule6) ((triple1 triple2) -> rule2)) -> rule3) OR ((triple1 ((((triple2) -> rule6) triple2) -> rule2)) -> rule3) OR ((((triple2) -> rule6) ((((triple2) -> rule6) triple2) -> rule2)) -> rule3))] Charlie is smart.[(((((triple3) -> rule6) triple3) -> rule2))] @3: Anne is rough.[(((((triple1 ((triple1 triple2) -> rule2)) -> rule3)) -> rule4) OR ((((((triple2) -> rule6) ((triple1 triple2) -> rule2)) -> rule3)) -> rule4) OR ((((triple1 ((((triple2) -> rule6) triple2) -> rule2)) -> rule3)) -> rule4) OR ((((((triple2) -> rule6) ((((triple2) -> rule6) triple2) -> rule2)) -> rule3)) -> rule4))] Charlie is green.[(((((triple3) -> rule6) ((((triple3) -> rule6) triple3) -> rule2)) -> rule3))] @4: Charlie is rough.[(((((((triple3) -> rule6) ((((triple3) -> rule6) triple3) -> rule2)) -> rule3)) -> rule4))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
((triple2) -> (rule6 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
triple2
Charlie is kind.
("Charlie" "is" "kind" "+")
triple3
Anne is smart.
("Anne" "is" "smart" "+")
((triple1 triple2) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
((((triple2) -> (rule6 % int2)) triple2) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
((triple3) -> (rule6 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
((triple1 ((triple1 triple2) -> (rule2 % int2))) -> (rule3 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
((((triple2) -> (rule6 % int3)) ((triple1 triple2) -> (rule2 % int2))) -> (rule3 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
((triple1 ((((triple2) -> (rule6 % int3)) triple2) -> (rule2 % int2))) -> (rule3 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
((((triple2) -> (rule6 % int3)) ((((triple2) -> (rule6 % int3)) triple2) -> (rule2 % int2))) -> (rule3 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Charlie is smart.
("Charlie" "is" "smart" "+")
((((triple3) -> (rule6 % int2)) triple3) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
((((triple1 ((triple1 triple2) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
((((((triple2) -> (rule6 % int4)) ((triple1 triple2) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is cold.
("Anne" "is" "cold" "+")
int4
((((triple1 ((((triple2) -> (rule6 % int4)) triple2) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is cold.
("Anne" "is" "cold" "+")
int4
((((((triple2) -> (rule6 % int4)) ((((triple2) -> (rule6 % int4)) triple2) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is cold.
("Anne" "is" "cold" "+")
int4
Charlie is green.
("Charlie" "is" "green" "+")
((((triple3) -> (rule6 % int3)) ((((triple3) -> (rule6 % int3)) triple3) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
Charlie is rough.
("Charlie" "is" "rough" "+")
((((((triple3) -> (rule6 % int4)) ((((triple3) -> (rule6 % int4)) triple3) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
Charlie is cold.
("Charlie" "is" "cold" "+")
int4