The cow is big. The cow is red. The cow sees the dog. The cow visits the squirrel. The dog eats the cow. The dog eats the lion. The dog sees the cow. The lion eats the cow. The lion eats the dog. The lion sees the cow. The lion sees the dog. The squirrel eats the cow. The squirrel eats the dog. The squirrel eats the lion. The squirrel sees the dog. If something is red and it sees the dog then the dog visits the lion. If the squirrel sees the lion then the squirrel visits the lion. If the dog sees the cow then the dog visits the cow. If something is red then it is rough. If something sees the lion and the lion visits the dog then the dog is young. If something visits the cow then it is red.
The cow is big.
("cow" "is" "big" "+")
The cow is red.
("cow" "is" "red" "+")
The cow sees the dog.
("cow" "sees" "dog" "+")
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
The dog eats the cow.
("dog" "eats" "cow" "+")
The dog eats the lion.
("dog" "eats" "lion" "+")
The dog sees the cow.
("dog" "sees" "cow" "+")
The lion eats the cow.
("lion" "eats" "cow" "+")
The lion eats the dog.
("lion" "eats" "dog" "+")
The lion sees the cow.
("lion" "sees" "cow" "+")
The lion sees the dog.
("lion" "sees" "dog" "+")
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
The squirrel eats the dog.
("squirrel" "eats" "dog" "+")
The squirrel eats the lion.
("squirrel" "eats" "lion" "+")
The squirrel sees the dog.
("squirrel" "sees" "dog" "+")
If something is red and it sees the dog then the dog visits the lion.
((("something" "is" "red" "+") ("something" "sees" "dog" "+")) -> ("dog" "visits" "lion" "+"))
If the squirrel sees the lion then the squirrel visits the lion.
((("squirrel" "sees" "lion" "+")) -> ("squirrel" "visits" "lion" "+"))
If the dog sees the cow then the dog visits the cow.
((("dog" "sees" "cow" "+")) -> ("dog" "visits" "cow" "+"))
If something is red then it is rough.
((("something" "is" "red" "+")) -> ("something" "is" "rough" "+"))
If something sees the lion and the lion visits the dog then the dog is young.
((("something" "sees" "lion" "+") ("lion" "visits" "dog" "+")) -> ("dog" "is" "young" "+"))
If something visits the cow then it is red.
((("something" "visits" "cow" "+")) -> ("something" "is" "red" "+"))
The lion eats the dog.
True
1
proof
[(triple9)]
("lion" "eats" "dog" "+")
triple9
The dog does not eat the lion.
False
1
inv-proof
[(triple6)]
("dog" "eats" "lion" "-")
triple6
The cow is rough.
True
2
proof
[(((triple2) -> rule4))]
("cow" "is" "rough" "+")
((triple2) -> (rule4 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The dog does not visit the lion.
False
3
inv-proof
[(((triple2 triple3) -> rule1))]
("dog" "visits" "lion" "-")
((triple2 triple3) -> (rule1 % int1))
The dog visits the lion.
("dog" "visits" "lion" "+")
int1
The dog is red.
True
3
proof
[(((((triple7) -> rule3)) -> rule6))]
("dog" "is" "red" "+")
((((triple7) -> (rule3 % int2))) -> (rule6 % int1))
The dog is red.
("dog" "is" "red" "+")
int1
The dog visits the cow.
("dog" "visits" "cow" "+")
int2
The dog is not red.
False
3
inv-proof
[(((((triple7) -> rule3)) -> rule6))]
("dog" "is" "red" "-")
((((triple7) -> (rule3 % int2))) -> (rule6 % int1))
The dog is red.
("dog" "is" "red" "+")
int1
The dog visits the cow.
("dog" "visits" "cow" "+")
int2
The dog is rough.
True
4
proof
[(((((((triple7) -> rule3)) -> rule6)) -> rule4))]
("dog" "is" "rough" "+")
((((((triple7) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The dog is red.
("dog" "is" "red" "+")
int2
The dog visits the cow.
("dog" "visits" "cow" "+")
int3
The dog is not rough.
False
4
inv-proof
[(((((((triple7) -> rule3)) -> rule6)) -> rule4))]
("dog" "is" "rough" "-")
((((((triple7) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The dog is red.
("dog" "is" "red" "+")
int2
The dog visits the cow.
("dog" "visits" "cow" "+")
int3
The dog is not young.
Unknown
inv-rconc
[@1: The dog is young.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("dog" "is" "young" "-")
The squirrel is rough.
Unknown
rconc
[@2: The squirrel is rough.[CWA. Example of deepest failure = (rule4 <- rule6 <- FAIL)]]
("squirrel" "is" "rough" "+")
The squirrel is not red.
Unknown
inv-rconc
[@1: The squirrel is red.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("squirrel" "is" "red" "-")
The lion is rough.
Unknown
rconc
[@2: The lion is rough.[CWA. Example of deepest failure = (rule4 <- rule6 <- FAIL)]]
("lion" "is" "rough" "+")
The dog does not eat the squirrel.
Unknown
inv-random
[@0: The dog eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "squirrel" "-")
The lion sees the squirrel.
Unknown
random
[@0: The lion sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "squirrel" "+")
The lion does not visit the cow.
Unknown
inv-random
[@0: The lion visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "cow" "-")
The cow visits the lion.
Unknown
random
[@0: The cow visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "lion" "+")
@0: The cow is big.[(triple1)] The cow is red.[(triple2)] The cow sees the dog.[(triple3)] The cow visits the squirrel.[(triple4)] The dog eats the cow.[(triple5)] The dog eats the lion.[(triple6)] The dog sees the cow.[(triple7)] The lion eats the cow.[(triple8)] The lion eats the dog.[(triple9)] The lion sees the cow.[(triple10)] The lion sees the dog.[(triple11)] The squirrel eats the cow.[(triple12)] The squirrel eats the dog.[(triple13)] The squirrel eats the lion.[(triple14)] The squirrel sees the dog.[(triple15)] @1: The cow is rough.[(((triple2) -> rule4))] The dog visits the cow.[(((triple7) -> rule3))] The dog visits the lion.[(((triple2 triple3) -> rule1))] @2: The dog is red.[(((((triple7) -> rule3)) -> rule6))] @3: The dog is rough.[(((((((triple7) -> rule3)) -> rule6)) -> rule4))]
The cow is big.
("cow" "is" "big" "+")
triple1
The cow is red.
("cow" "is" "red" "+")
triple2
The cow sees the dog.
("cow" "sees" "dog" "+")
triple3
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
triple4
The dog eats the cow.
("dog" "eats" "cow" "+")
triple5
The dog eats the lion.
("dog" "eats" "lion" "+")
triple6
The dog sees the cow.
("dog" "sees" "cow" "+")
triple7
The lion eats the cow.
("lion" "eats" "cow" "+")
triple8
The lion eats the dog.
("lion" "eats" "dog" "+")
triple9
The lion sees the cow.
("lion" "sees" "cow" "+")
triple10
The lion sees the dog.
("lion" "sees" "dog" "+")
triple11
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
triple12
The squirrel eats the dog.
("squirrel" "eats" "dog" "+")
triple13
The squirrel eats the lion.
("squirrel" "eats" "lion" "+")
triple14
The squirrel sees the dog.
("squirrel" "sees" "dog" "+")
triple15
The cow is rough.
("cow" "is" "rough" "+")
((triple2) -> (rule4 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The dog visits the cow.
("dog" "visits" "cow" "+")
((triple7) -> (rule3 % int1))
The dog visits the cow.
("dog" "visits" "cow" "+")
int1
The dog visits the lion.
("dog" "visits" "lion" "+")
((triple2 triple3) -> (rule1 % int1))
The dog visits the lion.
("dog" "visits" "lion" "+")
int1
The dog is red.
("dog" "is" "red" "+")
((((triple7) -> (rule3 % int2))) -> (rule6 % int1))
The dog is red.
("dog" "is" "red" "+")
int1
The dog visits the cow.
("dog" "visits" "cow" "+")
int2
The dog is rough.
("dog" "is" "rough" "+")
((((((triple7) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The dog is red.
("dog" "is" "red" "+")
int2
The dog visits the cow.
("dog" "visits" "cow" "+")
int3