The cat is big. The cat likes the tiger. The lion likes the mouse. The mouse is rough. The mouse needs the cat. The mouse needs the lion. The mouse visits the cat. The tiger is blue. The tiger visits the cat. The tiger visits the lion. If something is blue then it likes the mouse. If something is green and rough then it likes the lion. If something needs the tiger and the tiger is nice then it is rough. If something visits the cat then it is nice. If something needs the tiger then the tiger is green. If something needs the cat then the cat needs the tiger. If something is green and it likes the mouse then it needs the tiger.
The cat is big.
("cat" "is" "big" "+")
The cat likes the tiger.
("cat" "likes" "tiger" "+")
The lion likes the mouse.
("lion" "likes" "mouse" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The mouse needs the cat.
("mouse" "needs" "cat" "+")
The mouse needs the lion.
("mouse" "needs" "lion" "+")
The mouse visits the cat.
("mouse" "visits" "cat" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger visits the cat.
("tiger" "visits" "cat" "+")
The tiger visits the lion.
("tiger" "visits" "lion" "+")
If something is blue then it likes the mouse.
((("something" "is" "blue" "+")) -> ("something" "likes" "mouse" "+"))
If something is green and rough then it likes the lion.
((("something" "is" "green" "+") ("something" "is" "rough" "+")) -> ("something" "likes" "lion" "+"))
If something needs the tiger and the tiger is nice then it is rough.
((("something" "needs" "tiger" "+") ("tiger" "is" "nice" "+")) -> ("something" "is" "rough" "+"))
If something visits the cat then it is nice.
((("something" "visits" "cat" "+")) -> ("something" "is" "nice" "+"))
If something needs the tiger then the tiger is green.
((("something" "needs" "tiger" "+")) -> ("tiger" "is" "green" "+"))
If something needs the cat then the cat needs the tiger.
((("something" "needs" "cat" "+")) -> ("cat" "needs" "tiger" "+"))
If something is green and it likes the mouse then it needs the tiger.
((("something" "is" "green" "+") ("something" "likes" "mouse" "+")) -> ("something" "needs" "tiger" "+"))
The mouse is rough.
True
1
proof
[(triple4)]
("mouse" "is" "rough" "+")
triple4
The tiger does not visit the cat.
False
1
inv-proof
[(triple9)]
("tiger" "visits" "cat" "-")
triple9
The tiger is nice.
True
2
proof
[(((triple9) -> rule4))]
("tiger" "is" "nice" "+")
((triple9) -> (rule4 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
The mouse is not nice.
False
2
inv-proof
[(((triple7) -> rule4))]
("mouse" "is" "nice" "-")
((triple7) -> (rule4 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The tiger is green.
True
3
proof
[(((((triple5) -> rule6)) -> rule5))]
("tiger" "is" "green" "+")
((((triple5) -> (rule6 % int2))) -> (rule5 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The cat needs the tiger.
("cat" "needs" "tiger" "+")
int2
The tiger is not green.
False
3
inv-proof
[(((((triple5) -> rule6)) -> rule5))]
("tiger" "is" "green" "-")
((((triple5) -> (rule6 % int2))) -> (rule5 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The cat needs the tiger.
("cat" "needs" "tiger" "+")
int2
The tiger needs the tiger.
True
6
proof
[(((((((triple5) -> rule6)) -> rule5) ((triple8) -> rule1)) -> rule7))]
("tiger" "needs" "tiger" "+")
((((((triple5) -> (rule6 % int4))) -> (rule5 % int3)) ((triple8) -> (rule1 % int2))) -> (rule7 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
int2
The tiger is green.
("tiger" "is" "green" "+")
int3
The cat needs the tiger.
("cat" "needs" "tiger" "+")
int4
The tiger does not need the tiger.
False
6
inv-proof
[(((((((triple5) -> rule6)) -> rule5) ((triple8) -> rule1)) -> rule7))]
("tiger" "needs" "tiger" "-")
((((((triple5) -> (rule6 % int4))) -> (rule5 % int3)) ((triple8) -> (rule1 % int2))) -> (rule7 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
int2
The tiger is green.
("tiger" "is" "green" "+")
int3
The cat needs the tiger.
("cat" "needs" "tiger" "+")
int4
The tiger is rough.
True
9
proof
[(((((((((triple5) -> rule6)) -> rule5) ((triple8) -> rule1)) -> rule7) ((triple9) -> rule4)) -> rule3))]
("tiger" "is" "rough" "+")
((((((((triple5) -> (rule6 % int6))) -> (rule5 % int5)) ((triple8) -> (rule1 % int4))) -> (rule7 % int3)) ((triple9) -> (rule4 % int2))) -> (rule3 % int1))
The tiger is rough.
("tiger" "is" "rough" "+")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
int2
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int3
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
int4
The tiger is green.
("tiger" "is" "green" "+")
int5
The cat needs the tiger.
("cat" "needs" "tiger" "+")
int6
The tiger is not rough.
False
9
inv-proof
[(((((((((triple5) -> rule6)) -> rule5) ((triple8) -> rule1)) -> rule7) ((triple9) -> rule4)) -> rule3))]
("tiger" "is" "rough" "-")
((((((((triple5) -> (rule6 % int6))) -> (rule5 % int5)) ((triple8) -> (rule1 % int4))) -> (rule7 % int3)) ((triple9) -> (rule4 % int2))) -> (rule3 % int1))
The tiger is rough.
("tiger" "is" "rough" "+")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
int2
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int3
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
int4
The tiger is green.
("tiger" "is" "green" "+")
int5
The cat needs the tiger.
("cat" "needs" "tiger" "+")
int6
The tiger likes the lion.
True
13
proof
[(((((((triple5) -> rule6)) -> rule5) ((((((((triple5) -> rule6)) -> rule5) ((triple8) -> rule1)) -> rule7) ((triple9) -> rule4)) -> rule3)) -> rule2))]
("tiger" "likes" "lion" "+")
((((((triple5) -> (rule6 % int7))) -> (rule5 % int6)) ((((((((triple5) -> (rule6 % int7))) -> (rule5 % int6)) ((triple8) -> (rule1 % int5))) -> (rule7 % int4)) ((triple9) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The tiger likes the lion.
("tiger" "likes" "lion" "+")
int1
The tiger is rough.
("tiger" "is" "rough" "+")
int2
The tiger is nice.
("tiger" "is" "nice" "+")
int3
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int4
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
int5
The tiger is green.
("tiger" "is" "green" "+")
int6
The cat needs the tiger.
("cat" "needs" "tiger" "+")
int7
The tiger does not like the lion.
False
13
inv-proof
[(((((((triple5) -> rule6)) -> rule5) ((((((((triple5) -> rule6)) -> rule5) ((triple8) -> rule1)) -> rule7) ((triple9) -> rule4)) -> rule3)) -> rule2))]
("tiger" "likes" "lion" "-")
((((((triple5) -> (rule6 % int7))) -> (rule5 % int6)) ((((((((triple5) -> (rule6 % int7))) -> (rule5 % int6)) ((triple8) -> (rule1 % int5))) -> (rule7 % int4)) ((triple9) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The tiger likes the lion.
("tiger" "likes" "lion" "+")
int1
The tiger is rough.
("tiger" "is" "rough" "+")
int2
The tiger is nice.
("tiger" "is" "nice" "+")
int3
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int4
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
int5
The tiger is green.
("tiger" "is" "green" "+")
int6
The cat needs the tiger.
("cat" "needs" "tiger" "+")
int7
The cat does not like the lion.
Unknown
inv-rconc
[@1: The cat likes the lion.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "likes" "lion" "-")
The cat is nice.
Unknown
rconc
[@1: The cat is nice.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cat" "is" "nice" "+")
The mouse does not like the lion.
Unknown
inv-rconc
[@1: The mouse likes the lion.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "likes" "lion" "-")
The mouse likes the mouse.
Unknown
rconc
[@1: The mouse likes the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "likes" "mouse" "+")
The lion does not like the lion.
Unknown
inv-rconc
[@1: The lion likes the lion.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "likes" "lion" "-")
The lion needs the tiger.
Unknown
rconc
[@1: The lion needs the tiger.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("lion" "needs" "tiger" "+")
The lion does not need the cat.
Unknown
inv-random
[@0: The lion needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "cat" "-")
The lion is blue.
Unknown
random
[@0: The lion is blue.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "blue" "+")
The mouse is not blue.
Unknown
inv-random
[@0: The mouse is blue.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "blue" "-")
The lion needs the mouse.
Unknown
random
[@0: The lion needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "mouse" "+")
The cat does not visit the cat.
Unknown
inv-random
[@0: The cat visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "cat" "-")
The cat is green.
Unknown
random
[@0: The cat is green.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "green" "+")
@0: The cat is big.[(triple1)] The cat likes the tiger.[(triple2)] The lion likes the mouse.[(triple3)] The mouse is rough.[(triple4)] The mouse needs the cat.[(triple5)] The mouse needs the lion.[(triple6)] The mouse visits the cat.[(triple7)] The tiger is blue.[(triple8)] The tiger visits the cat.[(triple9)] The tiger visits the lion.[(triple10)] @1: The cat needs the tiger.[(((triple5) -> rule6))] The mouse is nice.[(((triple7) -> rule4))] The tiger is nice.[(((triple9) -> rule4))] The tiger likes the mouse.[(((triple8) -> rule1))] @2: The cat is rough.[(((((triple5) -> rule6) ((triple9) -> rule4)) -> rule3))] The tiger is green.[(((((triple5) -> rule6)) -> rule5))] @3: The tiger needs the tiger.[(((((((triple5) -> rule6)) -> rule5) ((triple8) -> rule1)) -> rule7))] @4: The tiger is rough.[(((((((((triple5) -> rule6)) -> rule5) ((triple8) -> rule1)) -> rule7) ((triple9) -> rule4)) -> rule3))] @5: The tiger likes the lion.[(((((((triple5) -> rule6)) -> rule5) ((((((((triple5) -> rule6)) -> rule5) ((triple8) -> rule1)) -> rule7) ((triple9) -> rule4)) -> rule3)) -> rule2))]
The cat is big.
("cat" "is" "big" "+")
triple1
The cat likes the tiger.
("cat" "likes" "tiger" "+")
triple2
The lion likes the mouse.
("lion" "likes" "mouse" "+")
triple3
The mouse is rough.
("mouse" "is" "rough" "+")
triple4
The mouse needs the cat.
("mouse" "needs" "cat" "+")
triple5
The mouse needs the lion.
("mouse" "needs" "lion" "+")
triple6
The mouse visits the cat.
("mouse" "visits" "cat" "+")
triple7
The tiger is blue.
("tiger" "is" "blue" "+")
triple8
The tiger visits the cat.
("tiger" "visits" "cat" "+")
triple9
The tiger visits the lion.
("tiger" "visits" "lion" "+")
triple10
The cat needs the tiger.
("cat" "needs" "tiger" "+")
((triple5) -> (rule6 % int1))
The cat needs the tiger.
("cat" "needs" "tiger" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
((triple7) -> (rule4 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
((triple9) -> (rule4 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
((triple8) -> (rule1 % int1))
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
int1
The cat is rough.
("cat" "is" "rough" "+")
((((triple5) -> (rule6 % int3)) ((triple9) -> (rule4 % int2))) -> (rule3 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
int2
The cat needs the tiger.
("cat" "needs" "tiger" "+")
int3
The tiger is green.
("tiger" "is" "green" "+")
((((triple5) -> (rule6 % int2))) -> (rule5 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The cat needs the tiger.
("cat" "needs" "tiger" "+")
int2
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
((((((triple5) -> (rule6 % int4))) -> (rule5 % int3)) ((triple8) -> (rule1 % int2))) -> (rule7 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
int2
The tiger is green.
("tiger" "is" "green" "+")
int3
The cat needs the tiger.
("cat" "needs" "tiger" "+")
int4
The tiger is rough.
("tiger" "is" "rough" "+")
((((((((triple5) -> (rule6 % int6))) -> (rule5 % int5)) ((triple8) -> (rule1 % int4))) -> (rule7 % int3)) ((triple9) -> (rule4 % int2))) -> (rule3 % int1))
The tiger is rough.
("tiger" "is" "rough" "+")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
int2
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int3
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
int4
The tiger is green.
("tiger" "is" "green" "+")
int5
The cat needs the tiger.
("cat" "needs" "tiger" "+")
int6
The tiger likes the lion.
("tiger" "likes" "lion" "+")
((((((triple5) -> (rule6 % int7))) -> (rule5 % int6)) ((((((((triple5) -> (rule6 % int7))) -> (rule5 % int6)) ((triple8) -> (rule1 % int5))) -> (rule7 % int4)) ((triple9) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The tiger likes the lion.
("tiger" "likes" "lion" "+")
int1
The tiger is rough.
("tiger" "is" "rough" "+")
int2
The tiger is nice.
("tiger" "is" "nice" "+")
int3
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int4
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
int5
The tiger is green.
("tiger" "is" "green" "+")
int6
The cat needs the tiger.
("cat" "needs" "tiger" "+")
int7