The bear chases the tiger. The cat does not chase the bear. The cat is big. The cat is green. The mouse chases the cat. The mouse chases the tiger. The mouse is red. The mouse is young. The mouse needs the bear. The mouse needs the tiger. The tiger chases the mouse. The tiger is big. The tiger is green. The tiger needs the bear. The tiger needs the cat. The tiger sees the mouse. If something chases the tiger and the tiger sees the cat then the cat sees the mouse. If something sees the bear then it chases the tiger. If something is young then it is nice. If something needs the mouse then it chases the bear. If something is nice then it chases the bear. If something needs the bear then the bear is nice. If something chases the bear then the bear needs the tiger. If something is green and not young then it chases the cat.
The bear chases the tiger.
("bear" "chases" "tiger" "+")
The cat does not chase the bear.
("cat" "chases" "bear" "-")
The cat is big.
("cat" "is" "big" "+")
The cat is green.
("cat" "is" "green" "+")
The mouse chases the cat.
("mouse" "chases" "cat" "+")
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
The mouse is red.
("mouse" "is" "red" "+")
The mouse is young.
("mouse" "is" "young" "+")
The mouse needs the bear.
("mouse" "needs" "bear" "+")
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger is green.
("tiger" "is" "green" "+")
The tiger needs the bear.
("tiger" "needs" "bear" "+")
The tiger needs the cat.
("tiger" "needs" "cat" "+")
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
If something chases the tiger and the tiger sees the cat then the cat sees the mouse.
((("something" "chases" "tiger" "+") ("tiger" "sees" "cat" "+")) -> ("cat" "sees" "mouse" "+"))
If something sees the bear then it chases the tiger.
((("something" "sees" "bear" "+")) -> ("something" "chases" "tiger" "+"))
If something is young then it is nice.
((("something" "is" "young" "+")) -> ("something" "is" "nice" "+"))
If something needs the mouse then it chases the bear.
((("something" "needs" "mouse" "+")) -> ("something" "chases" "bear" "+"))
If something is nice then it chases the bear.
((("something" "is" "nice" "+")) -> ("something" "chases" "bear" "+"))
If something needs the bear then the bear is nice.
((("something" "needs" "bear" "+")) -> ("bear" "is" "nice" "+"))
If something chases the bear then the bear needs the tiger.
((("something" "chases" "bear" "+")) -> ("bear" "needs" "tiger" "+"))
If something is green and not young then it chases the cat.
((("something" "is" "green" "+") ("something" "is" "young" "~")) -> ("something" "chases" "cat" "+"))
The cat is green.
True
1
proof
[(triple4)]
("cat" "is" "green" "+")
triple4
The tiger does not need the bear.
False
1
inv-proof
[(triple14)]
("tiger" "needs" "bear" "-")
triple14
The bear is nice.
True
2
proof
[(((triple14) -> rule6) OR ((triple9) -> rule6))]
("bear" "is" "nice" "+")
((triple14) -> (rule6 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
((triple9) -> (rule6 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The mouse is not nice.
False
2
inv-proof
[(((triple8) -> rule3))]
("mouse" "is" "nice" "-")
((triple8) -> (rule3 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The mouse chases the bear.
True
3
proof
[(((((triple8) -> rule3)) -> rule5))]
("mouse" "chases" "bear" "+")
((((triple8) -> (rule3 % int2))) -> (rule5 % int1))
The mouse chases the bear.
("mouse" "chases" "bear" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
int2
The mouse does not chase the bear.
False
3
inv-proof
[(((((triple8) -> rule3)) -> rule5))]
("mouse" "chases" "bear" "-")
((((triple8) -> (rule3 % int2))) -> (rule5 % int1))
The mouse chases the bear.
("mouse" "chases" "bear" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
int2
The bear needs the tiger.
True
4
proof
[(((((((triple14) -> rule6)) -> rule5)) -> rule7) OR ((((((triple8) -> rule3)) -> rule5)) -> rule7) OR ((((((triple9) -> rule6)) -> rule5)) -> rule7))]
("bear" "needs" "tiger" "+")
((((((triple14) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int1
The bear chases the bear.
("bear" "chases" "bear" "+")
int2
The bear is nice.
("bear" "is" "nice" "+")
int3
((((((triple8) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int1
The mouse chases the bear.
("mouse" "chases" "bear" "+")
int2
The mouse is nice.
("mouse" "is" "nice" "+")
int3
((((((triple9) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int1
The bear chases the bear.
("bear" "chases" "bear" "+")
int2
The bear is nice.
("bear" "is" "nice" "+")
int3
The bear does not need the tiger.
False
4
inv-proof
[(((((((triple14) -> rule6)) -> rule5)) -> rule7) OR ((((((triple8) -> rule3)) -> rule5)) -> rule7) OR ((((((triple9) -> rule6)) -> rule5)) -> rule7))]
("bear" "needs" "tiger" "-")
((((((triple14) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int1
The bear chases the bear.
("bear" "chases" "bear" "+")
int2
The bear is nice.
("bear" "is" "nice" "+")
int3
((((((triple8) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int1
The mouse chases the bear.
("mouse" "chases" "bear" "+")
int2
The mouse is nice.
("mouse" "is" "nice" "+")
int3
((((((triple9) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int1
The bear chases the bear.
("bear" "chases" "bear" "+")
int2
The bear is nice.
("bear" "is" "nice" "+")
int3
The tiger does not chase the tiger.
Unknown
inv-rconc
[@1: The tiger chases the tiger.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "chases" "tiger" "-")
The cat sees the mouse.
Unknown
rconc
[@1: The cat sees the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "sees" "mouse" "+")
The cat is not nice.
Unknown
inv-rconc
[@1: The cat is nice.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cat" "is" "nice" "-")
The tiger chases the cat.
Unknown
rconc
[@1: The tiger chases the cat.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("tiger" "chases" "cat" "+")
The mouse does not need the cat.
Unknown
inv-random
[@0: The mouse needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "cat" "-")
The mouse is big.
Unknown
random
[@0: The mouse is big.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "big" "+")
The bear is not big.
Unknown
inv-random
[@0: The bear is big.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "big" "-")
The cat sees the tiger.
Unknown
random
[@0: The cat sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "tiger" "+")
@0: The bear chases the tiger.[(triple1)] The cat does not chase the bear.[(triple2)] The cat is big.[(triple3)] The cat is green.[(triple4)] The mouse chases the cat.[(triple5)] The mouse chases the tiger.[(triple6)] The mouse is red.[(triple7)] The mouse is young.[(triple8)] The mouse needs the bear.[(triple9)] The mouse needs the tiger.[(triple10)] The tiger chases the mouse.[(triple11)] The tiger is big.[(triple12)] The tiger is green.[(triple13)] The tiger needs the bear.[(triple14)] The tiger needs the cat.[(triple15)] The tiger sees the mouse.[(triple16)] @1: The bear is nice.[(((triple14) -> rule6) OR ((triple9) -> rule6))] The mouse is nice.[(((triple8) -> rule3))] @2: The bear chases the bear.[(((((triple14) -> rule6)) -> rule5) OR ((((triple9) -> rule6)) -> rule5))] The mouse chases the bear.[(((((triple8) -> rule3)) -> rule5))] @3: The bear needs the tiger.[(((((((triple14) -> rule6)) -> rule5)) -> rule7) OR ((((((triple8) -> rule3)) -> rule5)) -> rule7) OR ((((((triple9) -> rule6)) -> rule5)) -> rule7))]
The bear chases the tiger.
("bear" "chases" "tiger" "+")
triple1
The cat does not chase the bear.
("cat" "chases" "bear" "-")
triple2
The cat is big.
("cat" "is" "big" "+")
triple3
The cat is green.
("cat" "is" "green" "+")
triple4
The mouse chases the cat.
("mouse" "chases" "cat" "+")
triple5
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
triple6
The mouse is red.
("mouse" "is" "red" "+")
triple7
The mouse is young.
("mouse" "is" "young" "+")
triple8
The mouse needs the bear.
("mouse" "needs" "bear" "+")
triple9
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
triple10
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
triple11
The tiger is big.
("tiger" "is" "big" "+")
triple12
The tiger is green.
("tiger" "is" "green" "+")
triple13
The tiger needs the bear.
("tiger" "needs" "bear" "+")
triple14
The tiger needs the cat.
("tiger" "needs" "cat" "+")
triple15
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
triple16
The bear is nice.
("bear" "is" "nice" "+")
((triple14) -> (rule6 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
((triple9) -> (rule6 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
((triple8) -> (rule3 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The bear chases the bear.
("bear" "chases" "bear" "+")
((((triple14) -> (rule6 % int2))) -> (rule5 % int1))
The bear chases the bear.
("bear" "chases" "bear" "+")
int1
The bear is nice.
("bear" "is" "nice" "+")
int2
((((triple9) -> (rule6 % int2))) -> (rule5 % int1))
The bear chases the bear.
("bear" "chases" "bear" "+")
int1
The bear is nice.
("bear" "is" "nice" "+")
int2
The mouse chases the bear.
("mouse" "chases" "bear" "+")
((((triple8) -> (rule3 % int2))) -> (rule5 % int1))
The mouse chases the bear.
("mouse" "chases" "bear" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
int2
The bear needs the tiger.
("bear" "needs" "tiger" "+")
((((((triple14) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int1
The bear chases the bear.
("bear" "chases" "bear" "+")
int2
The bear is nice.
("bear" "is" "nice" "+")
int3
((((((triple8) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int1
The mouse chases the bear.
("mouse" "chases" "bear" "+")
int2
The mouse is nice.
("mouse" "is" "nice" "+")
int3
((((((triple9) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int1
The bear chases the bear.
("bear" "chases" "bear" "+")
int2
The bear is nice.
("bear" "is" "nice" "+")
int3