The cow is green. The cow is round. The dog chases the cow. The dog chases the tiger. The dog eats the tiger. The squirrel eats the dog. The squirrel eats the tiger. The squirrel is blue. The squirrel is round. The squirrel visits the cow. The tiger chases the cow. The tiger visits the squirrel. If someone visits the squirrel and they eat the dog then the dog visits the squirrel. If someone eats the tiger then the tiger chases the squirrel. If someone is blue and they visit the tiger then the tiger is kind. If someone is kind then they chase the dog. If someone chases the squirrel and the squirrel visits the cow then they eat the squirrel. If someone chases the cow and the cow visits the tiger then the cow is green. If someone visits the tiger and the tiger eats the cow then they visit the cow. If someone visits the dog then they visit the cow. If someone eats the squirrel then the squirrel visits the tiger.
The cow is green.
("cow" "is" "green" "+")
The cow is round.
("cow" "is" "round" "+")
The dog chases the cow.
("dog" "chases" "cow" "+")
The dog chases the tiger.
("dog" "chases" "tiger" "+")
The dog eats the tiger.
("dog" "eats" "tiger" "+")
The squirrel eats the dog.
("squirrel" "eats" "dog" "+")
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
The squirrel is blue.
("squirrel" "is" "blue" "+")
The squirrel is round.
("squirrel" "is" "round" "+")
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
The tiger chases the cow.
("tiger" "chases" "cow" "+")
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
If someone visits the squirrel and they eat the dog then the dog visits the squirrel.
((("someone" "visits" "squirrel" "+") ("someone" "eats" "dog" "+")) -> ("dog" "visits" "squirrel" "+"))
If someone eats the tiger then the tiger chases the squirrel.
((("someone" "eats" "tiger" "+")) -> ("tiger" "chases" "squirrel" "+"))
If someone is blue and they visit the tiger then the tiger is kind.
((("someone" "is" "blue" "+") ("someone" "visits" "tiger" "+")) -> ("tiger" "is" "kind" "+"))
If someone is kind then they chase the dog.
((("someone" "is" "kind" "+")) -> ("someone" "chases" "dog" "+"))
If someone chases the squirrel and the squirrel visits the cow then they eat the squirrel.
((("someone" "chases" "squirrel" "+") ("squirrel" "visits" "cow" "+")) -> ("someone" "eats" "squirrel" "+"))
If someone chases the cow and the cow visits the tiger then the cow is green.
((("someone" "chases" "cow" "+") ("cow" "visits" "tiger" "+")) -> ("cow" "is" "green" "+"))
If someone visits the tiger and the tiger eats the cow then they visit the cow.
((("someone" "visits" "tiger" "+") ("tiger" "eats" "cow" "+")) -> ("someone" "visits" "cow" "+"))
If someone visits the dog then they visit the cow.
((("someone" "visits" "dog" "+")) -> ("someone" "visits" "cow" "+"))
If someone eats the squirrel then the squirrel visits the tiger.
((("someone" "eats" "squirrel" "+")) -> ("squirrel" "visits" "tiger" "+"))
The squirrel is blue.
True
1
proof
[(triple8)]
("squirrel" "is" "blue" "+")
triple8
The dog does not chase the cow.
False
1
inv-proof
[(triple3)]
("dog" "chases" "cow" "-")
triple3
The tiger chases the squirrel.
True
2
proof
[(((triple5) -> rule2) OR ((triple7) -> rule2))]
("tiger" "chases" "squirrel" "+")
((triple5) -> (rule2 % int1))
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
int1
((triple7) -> (rule2 % int1))
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
int1
The tiger does not chase the squirrel.
False
2
inv-proof
[(((triple5) -> rule2) OR ((triple7) -> rule2))]
("tiger" "chases" "squirrel" "-")
((triple5) -> (rule2 % int1))
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
int1
((triple7) -> (rule2 % int1))
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
int1
The tiger eats the squirrel.
True
4
proof
[(((((triple5) -> rule2) triple10) -> rule5) OR ((((triple7) -> rule2) triple10) -> rule5))]
("tiger" "eats" "squirrel" "+")
((((triple5) -> (rule2 % int2)) triple10) -> (rule5 % int1))
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
int1
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
int2
((((triple7) -> (rule2 % int2)) triple10) -> (rule5 % int1))
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
int1
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
int2
The tiger does not eat the squirrel.
False
4
inv-proof
[(((((triple5) -> rule2) triple10) -> rule5) OR ((((triple7) -> rule2) triple10) -> rule5))]
("tiger" "eats" "squirrel" "-")
((((triple5) -> (rule2 % int2)) triple10) -> (rule5 % int1))
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
int1
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
int2
((((triple7) -> (rule2 % int2)) triple10) -> (rule5 % int1))
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
int1
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
int2
The squirrel visits the tiger.
True
5
proof
[(((((((triple5) -> rule2) triple10) -> rule5)) -> rule9) OR ((((((triple7) -> rule2) triple10) -> rule5)) -> rule9))]
("squirrel" "visits" "tiger" "+")
((((((triple5) -> (rule2 % int3)) triple10) -> (rule5 % int2))) -> (rule9 % int1))
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
int1
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
int2
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
int3
((((((triple7) -> (rule2 % int3)) triple10) -> (rule5 % int2))) -> (rule9 % int1))
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
int1
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
int2
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
int3
The squirrel does not visit the tiger.
False
5
inv-proof
[(((((((triple5) -> rule2) triple10) -> rule5)) -> rule9) OR ((((((triple7) -> rule2) triple10) -> rule5)) -> rule9))]
("squirrel" "visits" "tiger" "-")
((((((triple5) -> (rule2 % int3)) triple10) -> (rule5 % int2))) -> (rule9 % int1))
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
int1
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
int2
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
int3
((((((triple7) -> (rule2 % int3)) triple10) -> (rule5 % int2))) -> (rule9 % int1))
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
int1
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
int2
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
int3
The tiger is kind.
True
7
proof
[(((triple8 ((((((triple5) -> rule2) triple10) -> rule5)) -> rule9)) -> rule3) OR ((triple8 ((((((triple7) -> rule2) triple10) -> rule5)) -> rule9)) -> rule3))]
("tiger" "is" "kind" "+")
((triple8 ((((((triple5) -> (rule2 % int4)) triple10) -> (rule5 % int3))) -> (rule9 % int2))) -> (rule3 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
int2
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
int3
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
int4
((triple8 ((((((triple7) -> (rule2 % int4)) triple10) -> (rule5 % int3))) -> (rule9 % int2))) -> (rule3 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
int2
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
int3
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
int4
The tiger is not kind.
False
7
inv-proof
[(((triple8 ((((((triple5) -> rule2) triple10) -> rule5)) -> rule9)) -> rule3) OR ((triple8 ((((((triple7) -> rule2) triple10) -> rule5)) -> rule9)) -> rule3))]
("tiger" "is" "kind" "-")
((triple8 ((((((triple5) -> (rule2 % int4)) triple10) -> (rule5 % int3))) -> (rule9 % int2))) -> (rule3 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
int2
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
int3
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
int4
((triple8 ((((((triple7) -> (rule2 % int4)) triple10) -> (rule5 % int3))) -> (rule9 % int2))) -> (rule3 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
int2
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
int3
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
int4
The tiger chases the dog.
True
8
proof
[(((((triple8 ((((((triple5) -> rule2) triple10) -> rule5)) -> rule9)) -> rule3)) -> rule4) OR ((((triple8 ((((((triple7) -> rule2) triple10) -> rule5)) -> rule9)) -> rule3)) -> rule4))]
("tiger" "chases" "dog" "+")
((((triple8 ((((((triple5) -> (rule2 % int5)) triple10) -> (rule5 % int4))) -> (rule9 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The tiger chases the dog.
("tiger" "chases" "dog" "+")
int1
The tiger is kind.
("tiger" "is" "kind" "+")
int2
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
int3
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
int4
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
int5
((((triple8 ((((((triple7) -> (rule2 % int5)) triple10) -> (rule5 % int4))) -> (rule9 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The tiger chases the dog.
("tiger" "chases" "dog" "+")
int1
The tiger is kind.
("tiger" "is" "kind" "+")
int2
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
int3
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
int4
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
int5
The tiger does not chase the dog.
False
8
inv-proof
[(((((triple8 ((((((triple5) -> rule2) triple10) -> rule5)) -> rule9)) -> rule3)) -> rule4) OR ((((triple8 ((((((triple7) -> rule2) triple10) -> rule5)) -> rule9)) -> rule3)) -> rule4))]
("tiger" "chases" "dog" "-")
((((triple8 ((((((triple5) -> (rule2 % int5)) triple10) -> (rule5 % int4))) -> (rule9 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The tiger chases the dog.
("tiger" "chases" "dog" "+")
int1
The tiger is kind.
("tiger" "is" "kind" "+")
int2
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
int3
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
int4
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
int5
((((triple8 ((((((triple7) -> (rule2 % int5)) triple10) -> (rule5 % int4))) -> (rule9 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The tiger chases the dog.
("tiger" "chases" "dog" "+")
int1
The tiger is kind.
("tiger" "is" "kind" "+")
int2
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
int3
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
int4
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
int5
The dog does not visit the cow.
Unknown
inv-rconc
[@1: The dog visits the cow.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("dog" "visits" "cow" "-")
The cow chases the dog.
Unknown
rconc
[@1: The cow chases the dog.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cow" "chases" "dog" "+")
The squirrel does not chase the dog.
Unknown
inv-rconc
[@1: The squirrel chases the dog.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("squirrel" "chases" "dog" "-")
The dog visits the squirrel.
Unknown
rconc
[@1: The dog visits the squirrel.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "visits" "squirrel" "+")
The dog does not chase the dog.
Unknown
inv-rconc
[@1: The dog chases the dog.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("dog" "chases" "dog" "-")
The dog eats the squirrel.
Unknown
rconc
[@1: The dog eats the squirrel.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("dog" "eats" "squirrel" "+")
The tiger does not eat the dog.
Unknown
inv-random
[@0: The tiger eats the dog.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "dog" "-")
The tiger visits the tiger.
Unknown
random
[@0: The tiger visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "tiger" "+")
The dog is not rough.
Unknown
inv-random
[@0: The dog is rough.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "rough" "-")
The cow visits the squirrel.
Unknown
random
[@0: The cow visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "squirrel" "+")
The dog is not kind.
Unknown
inv-random
[@0: The dog is kind.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "kind" "-")
The tiger is blue.
Unknown
random
[@0: The tiger is blue.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "blue" "+")
@0: The cow is green.[(triple1)] The cow is round.[(triple2)] The dog chases the cow.[(triple3)] The dog chases the tiger.[(triple4)] The dog eats the tiger.[(triple5)] The squirrel eats the dog.[(triple6)] The squirrel eats the tiger.[(triple7)] The squirrel is blue.[(triple8)] The squirrel is round.[(triple9)] The squirrel visits the cow.[(triple10)] The tiger chases the cow.[(triple11)] The tiger visits the squirrel.[(triple12)] @1: The tiger chases the squirrel.[(((triple5) -> rule2) OR ((triple7) -> rule2))] @2: The tiger eats the squirrel.[(((((triple5) -> rule2) triple10) -> rule5) OR ((((triple7) -> rule2) triple10) -> rule5))] @3: The squirrel visits the tiger.[(((((((triple5) -> rule2) triple10) -> rule5)) -> rule9) OR ((((((triple7) -> rule2) triple10) -> rule5)) -> rule9))] @4: The tiger is kind.[(((triple8 ((((((triple5) -> rule2) triple10) -> rule5)) -> rule9)) -> rule3) OR ((triple8 ((((((triple7) -> rule2) triple10) -> rule5)) -> rule9)) -> rule3))] @5: The tiger chases the dog.[(((((triple8 ((((((triple5) -> rule2) triple10) -> rule5)) -> rule9)) -> rule3)) -> rule4) OR ((((triple8 ((((((triple7) -> rule2) triple10) -> rule5)) -> rule9)) -> rule3)) -> rule4))]
The cow is green.
("cow" "is" "green" "+")
triple1
The cow is round.
("cow" "is" "round" "+")
triple2
The dog chases the cow.
("dog" "chases" "cow" "+")
triple3
The dog chases the tiger.
("dog" "chases" "tiger" "+")
triple4
The dog eats the tiger.
("dog" "eats" "tiger" "+")
triple5
The squirrel eats the dog.
("squirrel" "eats" "dog" "+")
triple6
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
triple7
The squirrel is blue.
("squirrel" "is" "blue" "+")
triple8
The squirrel is round.
("squirrel" "is" "round" "+")
triple9
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
triple10
The tiger chases the cow.
("tiger" "chases" "cow" "+")
triple11
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
triple12
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
((triple5) -> (rule2 % int1))
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
int1
((triple7) -> (rule2 % int1))
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
int1
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
((((triple5) -> (rule2 % int2)) triple10) -> (rule5 % int1))
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
int1
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
int2
((((triple7) -> (rule2 % int2)) triple10) -> (rule5 % int1))
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
int1
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
int2
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
((((((triple5) -> (rule2 % int3)) triple10) -> (rule5 % int2))) -> (rule9 % int1))
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
int1
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
int2
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
int3
((((((triple7) -> (rule2 % int3)) triple10) -> (rule5 % int2))) -> (rule9 % int1))
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
int1
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
int2
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
int3
The tiger is kind.
("tiger" "is" "kind" "+")
((triple8 ((((((triple5) -> (rule2 % int4)) triple10) -> (rule5 % int3))) -> (rule9 % int2))) -> (rule3 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
int2
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
int3
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
int4
((triple8 ((((((triple7) -> (rule2 % int4)) triple10) -> (rule5 % int3))) -> (rule9 % int2))) -> (rule3 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
int2
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
int3
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
int4
The tiger chases the dog.
("tiger" "chases" "dog" "+")
((((triple8 ((((((triple5) -> (rule2 % int5)) triple10) -> (rule5 % int4))) -> (rule9 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The tiger chases the dog.
("tiger" "chases" "dog" "+")
int1
The tiger is kind.
("tiger" "is" "kind" "+")
int2
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
int3
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
int4
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
int5
((((triple8 ((((((triple7) -> (rule2 % int5)) triple10) -> (rule5 % int4))) -> (rule9 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The tiger chases the dog.
("tiger" "chases" "dog" "+")
int1
The tiger is kind.
("tiger" "is" "kind" "+")
int2
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
int3
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
int4
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
int5