The cat chases the cow. The cat chases the tiger. The cat is not green. The cat does not need the cow. The cat needs the tiger. The cat visits the cow. The cat visits the tiger. The cow chases the tiger. The cow is rough. The cow needs the tiger. The cow does not visit the tiger. The tiger chases the cow. The tiger is blue. The tiger visits the cat. The tiger visits the cow. If someone chases the cow then they visit the cow. If someone is big and young then they do not need the cat. If someone chases the cow then the cow needs the cat. If someone visits the tiger then the tiger chases the cow. If someone chases the tiger then they chase the cow. If someone is young and they visit the tiger then they are not rough. If someone chases the cow then the cow is young. If the cat does not chase the cow then the cat needs the tiger.
The cat chases the cow.
("cat" "chases" "cow" "+")
The cat chases the tiger.
("cat" "chases" "tiger" "+")
The cat is not green.
("cat" "is" "green" "-")
The cat does not need the cow.
("cat" "needs" "cow" "-")
The cat needs the tiger.
("cat" "needs" "tiger" "+")
The cat visits the cow.
("cat" "visits" "cow" "+")
The cat visits the tiger.
("cat" "visits" "tiger" "+")
The cow chases the tiger.
("cow" "chases" "tiger" "+")
The cow is rough.
("cow" "is" "rough" "+")
The cow needs the tiger.
("cow" "needs" "tiger" "+")
The cow does not visit the tiger.
("cow" "visits" "tiger" "-")
The tiger chases the cow.
("tiger" "chases" "cow" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger visits the cat.
("tiger" "visits" "cat" "+")
The tiger visits the cow.
("tiger" "visits" "cow" "+")
If someone chases the cow then they visit the cow.
((("someone" "chases" "cow" "+")) -> ("someone" "visits" "cow" "+"))
If someone is big and young then they do not need the cat.
((("someone" "is" "big" "+") ("someone" "is" "young" "+")) -> ("someone" "needs" "cat" "-"))
If someone chases the cow then the cow needs the cat.
((("someone" "chases" "cow" "+")) -> ("cow" "needs" "cat" "+"))
If someone visits the tiger then the tiger chases the cow.
((("someone" "visits" "tiger" "+")) -> ("tiger" "chases" "cow" "+"))
If someone chases the tiger then they chase the cow.
((("someone" "chases" "tiger" "+")) -> ("someone" "chases" "cow" "+"))
If someone is young and they visit the tiger then they are not rough.
((("someone" "is" "young" "+") ("someone" "visits" "tiger" "+")) -> ("someone" "is" "rough" "-"))
If someone chases the cow then the cow is young.
((("someone" "chases" "cow" "+")) -> ("cow" "is" "young" "+"))
If the cat does not chase the cow then the cat needs the tiger.
((("cat" "chases" "cow" "~")) -> ("cat" "needs" "tiger" "+"))
The tiger visits the cat.
True
1
proof
[(triple14)]
("tiger" "visits" "cat" "+")
triple14
The tiger is not blue.
False
1
inv-proof
[(triple13)]
("tiger" "is" "blue" "-")
triple13
The cow needs the cat.
True
2
proof
[(((triple1) -> rule3) OR ((triple12) -> rule3) OR ((((triple2) -> rule5)) -> rule3) OR ((((triple7) -> rule4)) -> rule3) OR ((((triple8) -> rule5)) -> rule3))]
("cow" "needs" "cat" "+")
((triple1) -> (rule3 % int1))
The cow needs the cat.
("cow" "needs" "cat" "+")
int1
((triple12) -> (rule3 % int1))
The cow needs the cat.
("cow" "needs" "cat" "+")
int1
((((triple2) -> (rule5 % int2))) -> (rule3 % int1))
The cow needs the cat.
("cow" "needs" "cat" "+")
int1
The cat chases the cow.
("cat" "chases" "cow" "+")
int2
((((triple7) -> (rule4 % int2))) -> (rule3 % int1))
The cow needs the cat.
("cow" "needs" "cat" "+")
int1
The tiger chases the cow.
("tiger" "chases" "cow" "+")
int2
((((triple8) -> (rule5 % int2))) -> (rule3 % int1))
The cow needs the cat.
("cow" "needs" "cat" "+")
int1
The cow chases the cow.
("cow" "chases" "cow" "+")
int2
The cow does not need the cat.
False
2
inv-proof
[(((triple1) -> rule3) OR ((triple12) -> rule3) OR ((((triple2) -> rule5)) -> rule3) OR ((((triple7) -> rule4)) -> rule3) OR ((((triple8) -> rule5)) -> rule3))]
("cow" "needs" "cat" "-")
((triple1) -> (rule3 % int1))
The cow needs the cat.
("cow" "needs" "cat" "+")
int1
((triple12) -> (rule3 % int1))
The cow needs the cat.
("cow" "needs" "cat" "+")
int1
((((triple2) -> (rule5 % int2))) -> (rule3 % int1))
The cow needs the cat.
("cow" "needs" "cat" "+")
int1
The cat chases the cow.
("cat" "chases" "cow" "+")
int2
((((triple7) -> (rule4 % int2))) -> (rule3 % int1))
The cow needs the cat.
("cow" "needs" "cat" "+")
int1
The tiger chases the cow.
("tiger" "chases" "cow" "+")
int2
((((triple8) -> (rule5 % int2))) -> (rule3 % int1))
The cow needs the cat.
("cow" "needs" "cat" "+")
int1
The cow chases the cow.
("cow" "chases" "cow" "+")
int2
The cow visits the cow.
True
3
proof
[(((((triple8) -> rule5)) -> rule1))]
("cow" "visits" "cow" "+")
((((triple8) -> (rule5 % int2))) -> (rule1 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
The cow chases the cow.
("cow" "chases" "cow" "+")
int2
The cow does not visit the cow.
False
3
inv-proof
[(((((triple8) -> rule5)) -> rule1))]
("cow" "visits" "cow" "-")
((((triple8) -> (rule5 % int2))) -> (rule1 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
The cow chases the cow.
("cow" "chases" "cow" "+")
int2
The cow is not blue.
Unknown
inv-random
[@0: The cow is blue.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "blue" "-")
The cow is big.
Unknown
random
[@0: The cow is big.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "big" "+")
The tiger is not big.
Unknown
inv-random
[@0: The tiger is big.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "big" "-")
The cat visits the cat.
Unknown
random
[@0: The cat visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "cat" "+")
The cow does not visit the cat.
Unknown
inv-random
[@0: The cow visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "cat" "-")
The cat is young.
Unknown
random
[@0: The cat is young.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "young" "+")
@0: The cat chases the cow.[(triple1 OR ((triple2) -> rule5))] The cat chases the tiger.[(triple2)] The cat does not need the cow.[(triple4)] The cat is not green.[(triple3)] The cat needs the tiger.[(triple5)] The cat visits the cow.[(triple6 OR ((triple1) -> rule1) OR ((((triple2) -> rule5)) -> rule1))] The cat visits the tiger.[(triple7)] The cow chases the tiger.[(triple8)] The cow does not visit the tiger.[(triple11)] The cow is rough.[(triple9)] The cow needs the tiger.[(triple10)] The tiger chases the cow.[(triple12 OR ((triple7) -> rule4))] The tiger is blue.[(triple13)] The tiger visits the cat.[(triple14)] The tiger visits the cow.[(triple15 OR ((triple12) -> rule1) OR ((((triple7) -> rule4)) -> rule1))] @1: The cow chases the cow.[(((triple8) -> rule5))] The cow is young.[(((triple1) -> rule7) OR ((triple12) -> rule7) OR ((((triple2) -> rule5)) -> rule7) OR ((((triple7) -> rule4)) -> rule7) OR ((((triple8) -> rule5)) -> rule7))] The cow needs the cat.[(((triple1) -> rule3) OR ((triple12) -> rule3) OR ((((triple2) -> rule5)) -> rule3) OR ((((triple7) -> rule4)) -> rule3) OR ((((triple8) -> rule5)) -> rule3))] @2: The cow visits the cow.[(((((triple8) -> rule5)) -> rule1))]
The cat chases the cow.
("cat" "chases" "cow" "+")
triple1
((triple2) -> (rule5 % int1))
The cat chases the cow.
("cat" "chases" "cow" "+")
int1
The cat chases the tiger.
("cat" "chases" "tiger" "+")
triple2
The cat does not need the cow.
("cat" "needs" "cow" "-")
triple4
The cat is not green.
("cat" "is" "green" "-")
triple3
The cat needs the tiger.
("cat" "needs" "tiger" "+")
triple5
The cat visits the cow.
("cat" "visits" "cow" "+")
triple6
((triple1) -> (rule1 % int1))
The cat visits the cow.
("cat" "visits" "cow" "+")
int1
((((triple2) -> (rule5 % int2))) -> (rule1 % int1))
The cat visits the cow.
("cat" "visits" "cow" "+")
int1
The cat chases the cow.
("cat" "chases" "cow" "+")
int2
The cat visits the tiger.
("cat" "visits" "tiger" "+")
triple7
The cow chases the tiger.
("cow" "chases" "tiger" "+")
triple8
The cow does not visit the tiger.
("cow" "visits" "tiger" "-")
triple11
The cow is rough.
("cow" "is" "rough" "+")
triple9
The cow needs the tiger.
("cow" "needs" "tiger" "+")
triple10
The tiger chases the cow.
("tiger" "chases" "cow" "+")
triple12
((triple7) -> (rule4 % int1))
The tiger chases the cow.
("tiger" "chases" "cow" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
triple13
The tiger visits the cat.
("tiger" "visits" "cat" "+")
triple14
The tiger visits the cow.
("tiger" "visits" "cow" "+")
triple15
((triple12) -> (rule1 % int1))
The tiger visits the cow.
("tiger" "visits" "cow" "+")
int1
((((triple7) -> (rule4 % int2))) -> (rule1 % int1))
The tiger visits the cow.
("tiger" "visits" "cow" "+")
int1
The tiger chases the cow.
("tiger" "chases" "cow" "+")
int2
The cow chases the cow.
("cow" "chases" "cow" "+")
((triple8) -> (rule5 % int1))
The cow chases the cow.
("cow" "chases" "cow" "+")
int1
The cow is young.
("cow" "is" "young" "+")
((triple1) -> (rule7 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
((triple12) -> (rule7 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
((((triple2) -> (rule5 % int2))) -> (rule7 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The cat chases the cow.
("cat" "chases" "cow" "+")
int2
((((triple7) -> (rule4 % int2))) -> (rule7 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The tiger chases the cow.
("tiger" "chases" "cow" "+")
int2
((((triple8) -> (rule5 % int2))) -> (rule7 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The cow chases the cow.
("cow" "chases" "cow" "+")
int2
The cow needs the cat.
("cow" "needs" "cat" "+")
((triple1) -> (rule3 % int1))
The cow needs the cat.
("cow" "needs" "cat" "+")
int1
((triple12) -> (rule3 % int1))
The cow needs the cat.
("cow" "needs" "cat" "+")
int1
((((triple2) -> (rule5 % int2))) -> (rule3 % int1))
The cow needs the cat.
("cow" "needs" "cat" "+")
int1
The cat chases the cow.
("cat" "chases" "cow" "+")
int2
((((triple7) -> (rule4 % int2))) -> (rule3 % int1))
The cow needs the cat.
("cow" "needs" "cat" "+")
int1
The tiger chases the cow.
("tiger" "chases" "cow" "+")
int2
((((triple8) -> (rule5 % int2))) -> (rule3 % int1))
The cow needs the cat.
("cow" "needs" "cat" "+")
int1
The cow chases the cow.
("cow" "chases" "cow" "+")
int2
The cow visits the cow.
("cow" "visits" "cow" "+")
((((triple8) -> (rule5 % int2))) -> (rule1 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
The cow chases the cow.
("cow" "chases" "cow" "+")
int2