The bear needs the tiger. The dog chases the tiger. The dog is kind. The dog is red. The dog needs the bear. The dog sees the lion. The lion does not see the bear. The lion does not see the dog. The tiger is not big. The tiger needs the lion. The tiger sees the lion. If the bear needs the tiger then the tiger needs the dog. If something chases the lion then it is big. If something needs the bear then it sees the dog. If something needs the lion and the lion does not see the tiger then the lion is red. If something is blue and it sees the lion then it is red. If something is big then it chases the dog. If something needs the lion and it sees the dog then the dog is not red. If something sees the dog then it is rough. If something is rough and red then it chases the lion.
The bear needs the tiger.
("bear" "needs" "tiger" "+")
The dog chases the tiger.
("dog" "chases" "tiger" "+")
The dog is kind.
("dog" "is" "kind" "+")
The dog is red.
("dog" "is" "red" "+")
The dog needs the bear.
("dog" "needs" "bear" "+")
The dog sees the lion.
("dog" "sees" "lion" "+")
The lion does not see the bear.
("lion" "sees" "bear" "-")
The lion does not see the dog.
("lion" "sees" "dog" "-")
The tiger is not big.
("tiger" "is" "big" "-")
The tiger needs the lion.
("tiger" "needs" "lion" "+")
The tiger sees the lion.
("tiger" "sees" "lion" "+")
If the bear needs the tiger then the tiger needs the dog.
((("bear" "needs" "tiger" "+")) -> ("tiger" "needs" "dog" "+"))
If something chases the lion then it is big.
((("something" "chases" "lion" "+")) -> ("something" "is" "big" "+"))
If something needs the bear then it sees the dog.
((("something" "needs" "bear" "+")) -> ("something" "sees" "dog" "+"))
If something needs the lion and the lion does not see the tiger then the lion is red.
((("something" "needs" "lion" "+") ("lion" "sees" "tiger" "~")) -> ("lion" "is" "red" "+"))
If something is blue and it sees the lion then it is red.
((("something" "is" "blue" "+") ("something" "sees" "lion" "+")) -> ("something" "is" "red" "+"))
If something is big then it chases the dog.
((("something" "is" "big" "+")) -> ("something" "chases" "dog" "+"))
If something needs the lion and it sees the dog then the dog is not red.
((("something" "needs" "lion" "+") ("something" "sees" "dog" "+")) -> ("dog" "is" "red" "-"))
If something sees the dog then it is rough.
((("something" "sees" "dog" "+")) -> ("something" "is" "rough" "+"))
If something is rough and red then it chases the lion.
((("something" "is" "rough" "+") ("something" "is" "red" "+")) -> ("something" "chases" "lion" "+"))
The tiger sees the lion.
True
1
proof
[(triple11)]
("tiger" "sees" "lion" "+")
triple11
The dog is not kind.
False
1
inv-proof
[(triple3)]
("dog" "is" "kind" "-")
triple3
The tiger needs the dog.
True
2
proof
[(((triple1) -> rule1))]
("tiger" "needs" "dog" "+")
((triple1) -> (rule1 % int1))
The tiger needs the dog.
("tiger" "needs" "dog" "+")
int1
The dog does not see the dog.
False
2
inv-proof
[(((triple5) -> rule3))]
("dog" "sees" "dog" "-")
((triple5) -> (rule3 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
The dog is rough.
True
3
proof
[(((((triple5) -> rule3)) -> rule8))]
("dog" "is" "rough" "+")
((((triple5) -> (rule3 % int2))) -> (rule8 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The dog sees the dog.
("dog" "sees" "dog" "+")
int2
The dog is not rough.
False
3
inv-proof
[(((((triple5) -> rule3)) -> rule8))]
("dog" "is" "rough" "-")
((((triple5) -> (rule3 % int2))) -> (rule8 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The dog sees the dog.
("dog" "sees" "dog" "+")
int2
The dog chases the lion.
True
5
proof
[(((((((triple5) -> rule3)) -> rule8) triple4) -> rule9))]
("dog" "chases" "lion" "+")
((((((triple5) -> (rule3 % int3))) -> (rule8 % int2)) triple4) -> (rule9 % int1))
The dog chases the lion.
("dog" "chases" "lion" "+")
int1
The dog is rough.
("dog" "is" "rough" "+")
int2
The dog sees the dog.
("dog" "sees" "dog" "+")
int3
The dog does not chase the lion.
False
5
inv-proof
[(((((((triple5) -> rule3)) -> rule8) triple4) -> rule9))]
("dog" "chases" "lion" "-")
((((((triple5) -> (rule3 % int3))) -> (rule8 % int2)) triple4) -> (rule9 % int1))
The dog chases the lion.
("dog" "chases" "lion" "+")
int1
The dog is rough.
("dog" "is" "rough" "+")
int2
The dog sees the dog.
("dog" "sees" "dog" "+")
int3
The dog is big.
True
6
proof
[(((((((((triple5) -> rule3)) -> rule8) triple4) -> rule9)) -> rule2))]
("dog" "is" "big" "+")
((((((((triple5) -> (rule3 % int4))) -> (rule8 % int3)) triple4) -> (rule9 % int2))) -> (rule2 % int1))
The dog is big.
("dog" "is" "big" "+")
int1
The dog chases the lion.
("dog" "chases" "lion" "+")
int2
The dog is rough.
("dog" "is" "rough" "+")
int3
The dog sees the dog.
("dog" "sees" "dog" "+")
int4
The dog is not big.
False
6
inv-proof
[(((((((((triple5) -> rule3)) -> rule8) triple4) -> rule9)) -> rule2))]
("dog" "is" "big" "-")
((((((((triple5) -> (rule3 % int4))) -> (rule8 % int3)) triple4) -> (rule9 % int2))) -> (rule2 % int1))
The dog is big.
("dog" "is" "big" "+")
int1
The dog chases the lion.
("dog" "chases" "lion" "+")
int2
The dog is rough.
("dog" "is" "rough" "+")
int3
The dog sees the dog.
("dog" "sees" "dog" "+")
int4
The dog chases the dog.
True
7
proof
[(((((((((((triple5) -> rule3)) -> rule8) triple4) -> rule9)) -> rule2)) -> rule6))]
("dog" "chases" "dog" "+")
((((((((((triple5) -> (rule3 % int5))) -> (rule8 % int4)) triple4) -> (rule9 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The dog chases the dog.
("dog" "chases" "dog" "+")
int1
The dog is big.
("dog" "is" "big" "+")
int2
The dog chases the lion.
("dog" "chases" "lion" "+")
int3
The dog is rough.
("dog" "is" "rough" "+")
int4
The dog sees the dog.
("dog" "sees" "dog" "+")
int5
The dog does not chase the dog.
False
7
inv-proof
[(((((((((((triple5) -> rule3)) -> rule8) triple4) -> rule9)) -> rule2)) -> rule6))]
("dog" "chases" "dog" "-")
((((((((((triple5) -> (rule3 % int5))) -> (rule8 % int4)) triple4) -> (rule9 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The dog chases the dog.
("dog" "chases" "dog" "+")
int1
The dog is big.
("dog" "is" "big" "+")
int2
The dog chases the lion.
("dog" "chases" "lion" "+")
int3
The dog is rough.
("dog" "is" "rough" "+")
int4
The dog sees the dog.
("dog" "sees" "dog" "+")
int5
The lion is not red.
Unknown
inv-rconc
[@1: The lion is red.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("lion" "is" "red" "-")
The bear chases the lion.
Unknown
rconc
[@2: The bear chases the lion.[CWA. Example of deepest failure = (rule9 <- rule5 <- FAIL)]]
("bear" "chases" "lion" "+")
The tiger does not chase the lion.
Unknown
inv-rconc
[@2: The tiger chases the lion.[CWA. Example of deepest failure = (rule9 <- rule5 <- FAIL)]]
("tiger" "chases" "lion" "-")
The lion chases the lion.
Unknown
rconc
[@2: The lion chases the lion.[CWA. Example of deepest failure = (rule9 <- rule8 <- FAIL)]]
("lion" "chases" "lion" "+")
The bear does not chase the dog.
Unknown
inv-rconc
[@4: The bear chases the dog.[CWA. Example of deepest failure = (rule6 <- rule2 <- rule9 <- rule5 <- FAIL)]]
("bear" "chases" "dog" "-")
The bear is big.
Unknown
rconc
[@3: The bear is big.[CWA. Example of deepest failure = (rule2 <- rule9 <- rule5 <- FAIL)]]
("bear" "is" "big" "+")
The lion does not see the tiger.
Unknown
inv-random
[@0: The lion sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "tiger" "-")
The lion is kind.
Unknown
random
[@0: The lion is kind.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "kind" "+")
The dog does not see the bear.
Unknown
inv-random
[@0: The dog sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "bear" "-")
The lion needs the lion.
Unknown
random
[@0: The lion needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "lion" "+")
The bear does not see the bear.
Unknown
inv-random
[@0: The bear sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "bear" "-")
The lion sees the lion.
Unknown
random
[@0: The lion sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "lion" "+")
@0: The bear needs the tiger.[(triple1)] The dog chases the tiger.[(triple2)] The dog is kind.[(triple3)] The dog is red.[(triple4)] The dog needs the bear.[(triple5)] The dog sees the lion.[(triple6)] The lion does not see the bear.[(triple7)] The lion does not see the dog.[(triple8)] The tiger is not big.[(triple9)] The tiger needs the lion.[(triple10)] The tiger sees the lion.[(triple11)] @1: The dog sees the dog.[(((triple5) -> rule3))] The tiger needs the dog.[(((triple1) -> rule1))] @2: The dog is rough.[(((((triple5) -> rule3)) -> rule8))] @3: The dog chases the lion.[(((((((triple5) -> rule3)) -> rule8) triple4) -> rule9))] @4: The dog is big.[(((((((((triple5) -> rule3)) -> rule8) triple4) -> rule9)) -> rule2))] @5: The dog chases the dog.[(((((((((((triple5) -> rule3)) -> rule8) triple4) -> rule9)) -> rule2)) -> rule6))]
The bear needs the tiger.
("bear" "needs" "tiger" "+")
triple1
The dog chases the tiger.
("dog" "chases" "tiger" "+")
triple2
The dog is kind.
("dog" "is" "kind" "+")
triple3
The dog is red.
("dog" "is" "red" "+")
triple4
The dog needs the bear.
("dog" "needs" "bear" "+")
triple5
The dog sees the lion.
("dog" "sees" "lion" "+")
triple6
The lion does not see the bear.
("lion" "sees" "bear" "-")
triple7
The lion does not see the dog.
("lion" "sees" "dog" "-")
triple8
The tiger is not big.
("tiger" "is" "big" "-")
triple9
The tiger needs the lion.
("tiger" "needs" "lion" "+")
triple10
The tiger sees the lion.
("tiger" "sees" "lion" "+")
triple11
The dog sees the dog.
("dog" "sees" "dog" "+")
((triple5) -> (rule3 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
The tiger needs the dog.
("tiger" "needs" "dog" "+")
((triple1) -> (rule1 % int1))
The tiger needs the dog.
("tiger" "needs" "dog" "+")
int1
The dog is rough.
("dog" "is" "rough" "+")
((((triple5) -> (rule3 % int2))) -> (rule8 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The dog sees the dog.
("dog" "sees" "dog" "+")
int2
The dog chases the lion.
("dog" "chases" "lion" "+")
((((((triple5) -> (rule3 % int3))) -> (rule8 % int2)) triple4) -> (rule9 % int1))
The dog chases the lion.
("dog" "chases" "lion" "+")
int1
The dog is rough.
("dog" "is" "rough" "+")
int2
The dog sees the dog.
("dog" "sees" "dog" "+")
int3
The dog is big.
("dog" "is" "big" "+")
((((((((triple5) -> (rule3 % int4))) -> (rule8 % int3)) triple4) -> (rule9 % int2))) -> (rule2 % int1))
The dog is big.
("dog" "is" "big" "+")
int1
The dog chases the lion.
("dog" "chases" "lion" "+")
int2
The dog is rough.
("dog" "is" "rough" "+")
int3
The dog sees the dog.
("dog" "sees" "dog" "+")
int4
The dog chases the dog.
("dog" "chases" "dog" "+")
((((((((((triple5) -> (rule3 % int5))) -> (rule8 % int4)) triple4) -> (rule9 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The dog chases the dog.
("dog" "chases" "dog" "+")
int1
The dog is big.
("dog" "is" "big" "+")
int2
The dog chases the lion.
("dog" "chases" "lion" "+")
int3
The dog is rough.
("dog" "is" "rough" "+")
int4
The dog sees the dog.
("dog" "sees" "dog" "+")
int5