The cow is big. The cow is blue. The cow needs the tiger. The cow does not visit the dog. The dog visits the tiger. The mouse does not chase the cow. The tiger is not nice. If something visits the mouse then it chases the mouse. If the mouse does not chase the cow then the mouse needs the dog. If something chases the cow then the cow chases the tiger. If something needs the tiger and it chases the mouse then the tiger is not round. If the tiger is nice and the tiger is blue then the tiger chases the dog. If something chases the tiger and the tiger does not need the dog then the dog is big. If the mouse needs the dog then the dog visits the cow. If something visits the cow then the cow visits the mouse. If something is blue then it does not visit the cow.
The cow is big.
("cow" "is" "big" "+")
The cow is blue.
("cow" "is" "blue" "+")
The cow needs the tiger.
("cow" "needs" "tiger" "+")
The cow does not visit the dog.
("cow" "visits" "dog" "-")
The dog visits the tiger.
("dog" "visits" "tiger" "+")
The mouse does not chase the cow.
("mouse" "chases" "cow" "-")
The tiger is not nice.
("tiger" "is" "nice" "-")
If something visits the mouse then it chases the mouse.
((("something" "visits" "mouse" "+")) -> ("something" "chases" "mouse" "+"))
If the mouse does not chase the cow then the mouse needs the dog.
((("mouse" "chases" "cow" "~")) -> ("mouse" "needs" "dog" "+"))
If something chases the cow then the cow chases the tiger.
((("something" "chases" "cow" "+")) -> ("cow" "chases" "tiger" "+"))
If something needs the tiger and it chases the mouse then the tiger is not round.
((("something" "needs" "tiger" "+") ("something" "chases" "mouse" "+")) -> ("tiger" "is" "round" "-"))
If the tiger is nice and the tiger is blue then the tiger chases the dog.
((("tiger" "is" "nice" "+") ("tiger" "is" "blue" "+")) -> ("tiger" "chases" "dog" "+"))
If something chases the tiger and the tiger does not need the dog then the dog is big.
((("something" "chases" "tiger" "+") ("tiger" "needs" "dog" "~")) -> ("dog" "is" "big" "+"))
If the mouse needs the dog then the dog visits the cow.
((("mouse" "needs" "dog" "+")) -> ("dog" "visits" "cow" "+"))
If something visits the cow then the cow visits the mouse.
((("something" "visits" "cow" "+")) -> ("cow" "visits" "mouse" "+"))
If something is blue then it does not visit the cow.
((("something" "is" "blue" "+")) -> ("something" "visits" "cow" "-"))
The dog visits the tiger.
True
1
proof
[(triple5)]
("dog" "visits" "tiger" "+")
triple5
The tiger is nice.
False
1
inv-proof
[(triple7)]
("tiger" "is" "nice" "+")
triple7
The mouse needs the dog.
True
2
proof
[(((triple6) -> rule2))]
("mouse" "needs" "dog" "+")
((triple6) -> (rule2 % int1))
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int1
The mouse does not need the dog.
False
2
inv-proof
[(((triple6) -> rule2))]
("mouse" "needs" "dog" "-")
((triple6) -> (rule2 % int1))
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int1
The dog visits the cow.
True
3
proof
[(((((triple6) -> rule2)) -> rule7))]
("dog" "visits" "cow" "+")
((((triple6) -> (rule2 % int2))) -> (rule7 % int1))
The dog visits the cow.
("dog" "visits" "cow" "+")
int1
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int2
The dog does not visit the cow.
False
3
inv-proof
[(((((triple6) -> rule2)) -> rule7))]
("dog" "visits" "cow" "-")
((((triple6) -> (rule2 % int2))) -> (rule7 % int1))
The dog visits the cow.
("dog" "visits" "cow" "+")
int1
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int2
The cow visits the mouse.
True
4
proof
[(((((((triple6) -> rule2)) -> rule7)) -> rule8))]
("cow" "visits" "mouse" "+")
((((((triple6) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
The cow visits the mouse.
("cow" "visits" "mouse" "+")
int1
The dog visits the cow.
("dog" "visits" "cow" "+")
int2
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int3
The cow does not visit the mouse.
False
4
inv-proof
[(((((((triple6) -> rule2)) -> rule7)) -> rule8))]
("cow" "visits" "mouse" "-")
((((((triple6) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
The cow visits the mouse.
("cow" "visits" "mouse" "+")
int1
The dog visits the cow.
("dog" "visits" "cow" "+")
int2
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int3
The cow chases the mouse.
True
5
proof
[(((((((((triple6) -> rule2)) -> rule7)) -> rule8)) -> rule1))]
("cow" "chases" "mouse" "+")
((((((((triple6) -> (rule2 % int4))) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
The cow chases the mouse.
("cow" "chases" "mouse" "+")
int1
The cow visits the mouse.
("cow" "visits" "mouse" "+")
int2
The dog visits the cow.
("dog" "visits" "cow" "+")
int3
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int4
The cow does not chase the mouse.
False
5
inv-proof
[(((((((((triple6) -> rule2)) -> rule7)) -> rule8)) -> rule1))]
("cow" "chases" "mouse" "-")
((((((((triple6) -> (rule2 % int4))) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
The cow chases the mouse.
("cow" "chases" "mouse" "+")
int1
The cow visits the mouse.
("cow" "visits" "mouse" "+")
int2
The dog visits the cow.
("dog" "visits" "cow" "+")
int3
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int4
The tiger is not round.
True
7
proof
[(((triple3 ((((((((triple6) -> rule2)) -> rule7)) -> rule8)) -> rule1)) -> rule4))]
("tiger" "is" "round" "-")
((triple3 ((((((((triple6) -> (rule2 % int5))) -> (rule7 % int4))) -> (rule8 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The tiger is not round.
("tiger" "is" "round" "-")
int1
The cow chases the mouse.
("cow" "chases" "mouse" "+")
int2
The cow visits the mouse.
("cow" "visits" "mouse" "+")
int3
The dog visits the cow.
("dog" "visits" "cow" "+")
int4
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int5
The tiger is round.
False
7
inv-proof
[(((triple3 ((((((((triple6) -> rule2)) -> rule7)) -> rule8)) -> rule1)) -> rule4))]
("tiger" "is" "round" "+")
((triple3 ((((((((triple6) -> (rule2 % int5))) -> (rule7 % int4))) -> (rule8 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The tiger is not round.
("tiger" "is" "round" "-")
int1
The cow chases the mouse.
("cow" "chases" "mouse" "+")
int2
The cow visits the mouse.
("cow" "visits" "mouse" "+")
int3
The dog visits the cow.
("dog" "visits" "cow" "+")
int4
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int5
The dog does not chase the mouse.
Unknown
inv-rconc
[@1: The dog chases the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "chases" "mouse" "-")
The mouse chases the mouse.
Unknown
rconc
[@1: The mouse chases the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "chases" "mouse" "+")
The cow does not chase the tiger.
Unknown
inv-rconc
[@1: The cow chases the tiger.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cow" "chases" "tiger" "-")
The dog is big.
Unknown
rconc
[@1: The dog is big.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("dog" "is" "big" "+")
The tiger does not chase the mouse.
Unknown
inv-rconc
[@1: The tiger chases the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "chases" "mouse" "-")
The tiger chases the dog.
Unknown
rconc
[@1: The tiger chases the dog.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("tiger" "chases" "dog" "+")
The tiger does not need the dog.
Unknown
inv-random
[@0: The tiger needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "dog" "-")
The cow visits the tiger.
Unknown
random
[@0: The cow visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "tiger" "+")
The tiger does not chase the tiger.
Unknown
inv-random
[@0: The tiger chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "tiger" "-")
The tiger needs the cow.
Unknown
random
[@0: The tiger needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "cow" "+")
The cow does not need the mouse.
Unknown
inv-random
[@0: The cow needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "mouse" "-")
The tiger needs the mouse.
Unknown
random
[@0: The tiger needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "mouse" "+")
@0: The cow does not visit the dog.[(triple4)] The cow is big.[(triple1)] The cow is blue.[(triple2)] The cow needs the tiger.[(triple3)] The dog visits the tiger.[(triple5)] The mouse does not chase the cow.[(triple6)] The tiger is not nice.[(triple7)] @1: The cow does not visit the cow.[(((triple2) -> rule9))] The mouse needs the dog.[(((triple6) -> rule2))] @2: The dog visits the cow.[(((((triple6) -> rule2)) -> rule7))] @3: The cow visits the mouse.[(((((((triple6) -> rule2)) -> rule7)) -> rule8))] @4: The cow chases the mouse.[(((((((((triple6) -> rule2)) -> rule7)) -> rule8)) -> rule1))] @5: The tiger is not round.[(((triple3 ((((((((triple6) -> rule2)) -> rule7)) -> rule8)) -> rule1)) -> rule4))]
The cow does not visit the dog.
("cow" "visits" "dog" "-")
triple4
The cow is big.
("cow" "is" "big" "+")
triple1
The cow is blue.
("cow" "is" "blue" "+")
triple2
The cow needs the tiger.
("cow" "needs" "tiger" "+")
triple3
The dog visits the tiger.
("dog" "visits" "tiger" "+")
triple5
The mouse does not chase the cow.
("mouse" "chases" "cow" "-")
triple6
The tiger is not nice.
("tiger" "is" "nice" "-")
triple7
The cow does not visit the cow.
("cow" "visits" "cow" "-")
((triple2) -> (rule9 % int1))
The cow does not visit the cow.
("cow" "visits" "cow" "-")
int1
The mouse needs the dog.
("mouse" "needs" "dog" "+")
((triple6) -> (rule2 % int1))
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int1
The dog visits the cow.
("dog" "visits" "cow" "+")
((((triple6) -> (rule2 % int2))) -> (rule7 % int1))
The dog visits the cow.
("dog" "visits" "cow" "+")
int1
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int2
The cow visits the mouse.
("cow" "visits" "mouse" "+")
((((((triple6) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
The cow visits the mouse.
("cow" "visits" "mouse" "+")
int1
The dog visits the cow.
("dog" "visits" "cow" "+")
int2
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int3
The cow chases the mouse.
("cow" "chases" "mouse" "+")
((((((((triple6) -> (rule2 % int4))) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
The cow chases the mouse.
("cow" "chases" "mouse" "+")
int1
The cow visits the mouse.
("cow" "visits" "mouse" "+")
int2
The dog visits the cow.
("dog" "visits" "cow" "+")
int3
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int4
The tiger is not round.
("tiger" "is" "round" "-")
((triple3 ((((((((triple6) -> (rule2 % int5))) -> (rule7 % int4))) -> (rule8 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The tiger is not round.
("tiger" "is" "round" "-")
int1
The cow chases the mouse.
("cow" "chases" "mouse" "+")
int2
The cow visits the mouse.
("cow" "visits" "mouse" "+")
int3
The dog visits the cow.
("dog" "visits" "cow" "+")
int4
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int5