The bear is cold. The bear is red. The bear does not need the cat. The bear sees the lion. The cat is not cold. The cat is not round. The cat does not see the lion. The cat sees the mouse. The lion visits the bear. The mouse is red. The mouse is not rough. If something is kind then it sees the cat. If something visits the bear then it is kind. If something is rough and it needs the mouse then the mouse visits the bear. If something sees the cat then the cat visits the bear. If something sees the cat and the cat visits the bear then the bear does not visit the lion. If something sees the mouse and it does not need the mouse then the mouse needs the cat. If something visits the lion and it does not see the mouse then the mouse is cold.
The bear is cold.
("bear" "is" "cold" "+")
The bear is red.
("bear" "is" "red" "+")
The bear does not need the cat.
("bear" "needs" "cat" "-")
The bear sees the lion.
("bear" "sees" "lion" "+")
The cat is not cold.
("cat" "is" "cold" "-")
The cat is not round.
("cat" "is" "round" "-")
The cat does not see the lion.
("cat" "sees" "lion" "-")
The cat sees the mouse.
("cat" "sees" "mouse" "+")
The lion visits the bear.
("lion" "visits" "bear" "+")
The mouse is red.
("mouse" "is" "red" "+")
The mouse is not rough.
("mouse" "is" "rough" "-")
If something is kind then it sees the cat.
((("something" "is" "kind" "+")) -> ("something" "sees" "cat" "+"))
If something visits the bear then it is kind.
((("something" "visits" "bear" "+")) -> ("something" "is" "kind" "+"))
If something is rough and it needs the mouse then the mouse visits the bear.
((("something" "is" "rough" "+") ("something" "needs" "mouse" "+")) -> ("mouse" "visits" "bear" "+"))
If something sees the cat then the cat visits the bear.
((("something" "sees" "cat" "+")) -> ("cat" "visits" "bear" "+"))
If something sees the cat and the cat visits the bear then the bear does not visit the lion.
((("something" "sees" "cat" "+") ("cat" "visits" "bear" "+")) -> ("bear" "visits" "lion" "-"))
If something sees the mouse and it does not need the mouse then the mouse needs the cat.
((("something" "sees" "mouse" "+") ("something" "needs" "mouse" "~")) -> ("mouse" "needs" "cat" "+"))
If something visits the lion and it does not see the mouse then the mouse is cold.
((("something" "visits" "lion" "+") ("something" "sees" "mouse" "~")) -> ("mouse" "is" "cold" "+"))
The bear is red.
True
1
proof
[(triple2)]
("bear" "is" "red" "+")
triple2
The bear does not see the lion.
False
1
inv-proof
[(triple4)]
("bear" "sees" "lion" "-")
triple4
The lion is kind.
True
2
proof
[(((triple9) -> rule2))]
("lion" "is" "kind" "+")
((triple9) -> (rule2 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion is not kind.
False
2
inv-proof
[(((triple9) -> rule2))]
("lion" "is" "kind" "-")
((triple9) -> (rule2 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion sees the cat.
True
3
proof
[(((((triple9) -> rule2)) -> rule1))]
("lion" "sees" "cat" "+")
((((triple9) -> (rule2 % int2))) -> (rule1 % int1))
The lion sees the cat.
("lion" "sees" "cat" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2
The lion does not see the cat.
False
3
inv-proof
[(((((triple9) -> rule2)) -> rule1))]
("lion" "sees" "cat" "-")
((((triple9) -> (rule2 % int2))) -> (rule1 % int1))
The lion sees the cat.
("lion" "sees" "cat" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2
The cat visits the bear.
True
4
proof
[(((((((triple9) -> rule2)) -> rule1)) -> rule4))]
("cat" "visits" "bear" "+")
((((((triple9) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The cat visits the bear.
("cat" "visits" "bear" "+")
int1
The lion sees the cat.
("lion" "sees" "cat" "+")
int2
The lion is kind.
("lion" "is" "kind" "+")
int3
The cat does not visit the bear.
False
4
inv-proof
[(((((((triple9) -> rule2)) -> rule1)) -> rule4))]
("cat" "visits" "bear" "-")
((((((triple9) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The cat visits the bear.
("cat" "visits" "bear" "+")
int1
The lion sees the cat.
("lion" "sees" "cat" "+")
int2
The lion is kind.
("lion" "is" "kind" "+")
int3
The bear does not visit the lion.
True
8
proof
[(((((((triple9) -> rule2)) -> rule1) ((((((triple9) -> rule2)) -> rule1)) -> rule4)) -> rule5) OR ((((((((((((triple9) -> rule2)) -> rule1)) -> rule4)) -> rule2)) -> rule1) ((((((triple9) -> rule2)) -> rule1)) -> rule4)) -> rule5))]
("bear" "visits" "lion" "-")
((((((triple9) -> (rule2 % int4))) -> (rule1 % int3)) ((((((triple9) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The bear does not visit the lion.
("bear" "visits" "lion" "-")
int1
The cat visits the bear.
("cat" "visits" "bear" "+")
int2
The lion sees the cat.
("lion" "sees" "cat" "+")
int3
The lion is kind.
("lion" "is" "kind" "+")
int4
((((((((((((triple9) -> (rule2 % int6))) -> (rule1 % int5))) -> (rule4 % int4))) -> (rule2 % int3))) -> (rule1 % int2)) ((((((triple9) -> (rule2 % int6))) -> (rule1 % int5))) -> (rule4 % int4))) -> (rule5 % int1))
The bear does not visit the lion.
("bear" "visits" "lion" "-")
int1
The cat sees the cat.
("cat" "sees" "cat" "+")
int2
The cat is kind.
("cat" "is" "kind" "+")
int3
The cat visits the bear.
("cat" "visits" "bear" "+")
int4
The lion sees the cat.
("lion" "sees" "cat" "+")
int5
The lion is kind.
("lion" "is" "kind" "+")
int6
The cat is not kind.
False
5
inv-proof
[(((((((((triple9) -> rule2)) -> rule1)) -> rule4)) -> rule2))]
("cat" "is" "kind" "-")
((((((((triple9) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The cat visits the bear.
("cat" "visits" "bear" "+")
int2
The lion sees the cat.
("lion" "sees" "cat" "+")
int3
The lion is kind.
("lion" "is" "kind" "+")
int4
The cat sees the cat.
True
6
proof
[(((((((((((triple9) -> rule2)) -> rule1)) -> rule4)) -> rule2)) -> rule1))]
("cat" "sees" "cat" "+")
((((((((((triple9) -> (rule2 % int5))) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The cat is kind.
("cat" "is" "kind" "+")
int2
The cat visits the bear.
("cat" "visits" "bear" "+")
int3
The lion sees the cat.
("lion" "sees" "cat" "+")
int4
The lion is kind.
("lion" "is" "kind" "+")
int5
The cat does not see the cat.
False
6
inv-proof
[(((((((((((triple9) -> rule2)) -> rule1)) -> rule4)) -> rule2)) -> rule1))]
("cat" "sees" "cat" "-")
((((((((((triple9) -> (rule2 % int5))) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The cat is kind.
("cat" "is" "kind" "+")
int2
The cat visits the bear.
("cat" "visits" "bear" "+")
int3
The lion sees the cat.
("lion" "sees" "cat" "+")
int4
The lion is kind.
("lion" "is" "kind" "+")
int5
The mouse is not kind.
Unknown
inv-rconc
[@2: The mouse is kind.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("mouse" "is" "kind" "-")
The bear sees the cat.
Unknown
rconc
[@2: The bear sees the cat.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("bear" "sees" "cat" "+")
The bear is not kind.
Unknown
inv-rconc
[@1: The bear is kind.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "is" "kind" "-")
The mouse visits the bear.
Unknown
rconc
[@1: The mouse visits the bear.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "visits" "bear" "+")
The mouse does not need the cat.
Unknown
inv-rconc
[@1: The mouse needs the cat.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("mouse" "needs" "cat" "-")
The mouse is cold.
Unknown
rconc
[@1: The mouse is cold.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("mouse" "is" "cold" "+")
The mouse does not visit the lion.
Unknown
inv-random
[@0: The mouse visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "lion" "-")
The cat needs the cat.
Unknown
random
[@0: The cat needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "cat" "+")
The bear does not visit the mouse.
Unknown
inv-random
[@0: The bear visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "mouse" "-")
The bear needs the bear.
Unknown
random
[@0: The bear needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "bear" "+")
The lion is not red.
Unknown
inv-random
[@0: The lion is red.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "red" "-")
The lion is rough.
Unknown
random
[@0: The lion is rough.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "rough" "+")
@0: The bear does not need the cat.[(triple3)] The bear is cold.[(triple1)] The bear is red.[(triple2)] The bear sees the lion.[(triple4)] The cat does not see the lion.[(triple7)] The cat is not cold.[(triple5)] The cat is not round.[(triple6)] The cat sees the mouse.[(triple8)] The lion visits the bear.[(triple9)] The mouse is not rough.[(triple11)] The mouse is red.[(triple10)] @1: The lion is kind.[(((triple9) -> rule2))] @2: The lion sees the cat.[(((((triple9) -> rule2)) -> rule1))] @3: The cat visits the bear.[(((((((triple9) -> rule2)) -> rule1)) -> rule4))] @4: The bear does not visit the lion.[(((((((triple9) -> rule2)) -> rule1) ((((((triple9) -> rule2)) -> rule1)) -> rule4)) -> rule5) OR ((((((((((((triple9) -> rule2)) -> rule1)) -> rule4)) -> rule2)) -> rule1) ((((((triple9) -> rule2)) -> rule1)) -> rule4)) -> rule5))] The cat is kind.[(((((((((triple9) -> rule2)) -> rule1)) -> rule4)) -> rule2))] @5: The cat sees the cat.[(((((((((((triple9) -> rule2)) -> rule1)) -> rule4)) -> rule2)) -> rule1))]
The bear does not need the cat.
("bear" "needs" "cat" "-")
triple3
The bear is cold.
("bear" "is" "cold" "+")
triple1
The bear is red.
("bear" "is" "red" "+")
triple2
The bear sees the lion.
("bear" "sees" "lion" "+")
triple4
The cat does not see the lion.
("cat" "sees" "lion" "-")
triple7
The cat is not cold.
("cat" "is" "cold" "-")
triple5
The cat is not round.
("cat" "is" "round" "-")
triple6
The cat sees the mouse.
("cat" "sees" "mouse" "+")
triple8
The lion visits the bear.
("lion" "visits" "bear" "+")
triple9
The mouse is not rough.
("mouse" "is" "rough" "-")
triple11
The mouse is red.
("mouse" "is" "red" "+")
triple10
The lion is kind.
("lion" "is" "kind" "+")
((triple9) -> (rule2 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion sees the cat.
("lion" "sees" "cat" "+")
((((triple9) -> (rule2 % int2))) -> (rule1 % int1))
The lion sees the cat.
("lion" "sees" "cat" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2
The cat visits the bear.
("cat" "visits" "bear" "+")
((((((triple9) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The cat visits the bear.
("cat" "visits" "bear" "+")
int1
The lion sees the cat.
("lion" "sees" "cat" "+")
int2
The lion is kind.
("lion" "is" "kind" "+")
int3
The bear does not visit the lion.
("bear" "visits" "lion" "-")
((((((triple9) -> (rule2 % int4))) -> (rule1 % int3)) ((((((triple9) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The bear does not visit the lion.
("bear" "visits" "lion" "-")
int1
The cat visits the bear.
("cat" "visits" "bear" "+")
int2
The lion sees the cat.
("lion" "sees" "cat" "+")
int3
The lion is kind.
("lion" "is" "kind" "+")
int4
((((((((((((triple9) -> (rule2 % int6))) -> (rule1 % int5))) -> (rule4 % int4))) -> (rule2 % int3))) -> (rule1 % int2)) ((((((triple9) -> (rule2 % int6))) -> (rule1 % int5))) -> (rule4 % int4))) -> (rule5 % int1))
The bear does not visit the lion.
("bear" "visits" "lion" "-")
int1
The cat sees the cat.
("cat" "sees" "cat" "+")
int2
The cat is kind.
("cat" "is" "kind" "+")
int3
The cat visits the bear.
("cat" "visits" "bear" "+")
int4
The lion sees the cat.
("lion" "sees" "cat" "+")
int5
The lion is kind.
("lion" "is" "kind" "+")
int6
The cat is kind.
("cat" "is" "kind" "+")
((((((((triple9) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The cat visits the bear.
("cat" "visits" "bear" "+")
int2
The lion sees the cat.
("lion" "sees" "cat" "+")
int3
The lion is kind.
("lion" "is" "kind" "+")
int4
The cat sees the cat.
("cat" "sees" "cat" "+")
((((((((((triple9) -> (rule2 % int5))) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The cat is kind.
("cat" "is" "kind" "+")
int2
The cat visits the bear.
("cat" "visits" "bear" "+")
int3
The lion sees the cat.
("lion" "sees" "cat" "+")
int4
The lion is kind.
("lion" "is" "kind" "+")
int5