The cat eats the dog. The cat is blue. The cat sees the dog. The cat visits the cow. The cow visits the cat. The dog eats the cat. The dog visits the lion. The lion eats the cow. The lion sees the cat. The lion sees the cow. The lion visits the cat. The lion visits the cow. If something visits the dog and it sees the cat then the cat does not see the lion. If the lion visits the cow then the lion visits the dog.
The cat eats the dog.
("cat" "eats" "dog" "+")
The cat is blue.
("cat" "is" "blue" "+")
The cat sees the dog.
("cat" "sees" "dog" "+")
The cat visits the cow.
("cat" "visits" "cow" "+")
The cow visits the cat.
("cow" "visits" "cat" "+")
The dog eats the cat.
("dog" "eats" "cat" "+")
The dog visits the lion.
("dog" "visits" "lion" "+")
The lion eats the cow.
("lion" "eats" "cow" "+")
The lion sees the cat.
("lion" "sees" "cat" "+")
The lion sees the cow.
("lion" "sees" "cow" "+")
The lion visits the cat.
("lion" "visits" "cat" "+")
The lion visits the cow.
("lion" "visits" "cow" "+")
If something visits the dog and it sees the cat then the cat does not see the lion.
((("something" "visits" "dog" "+") ("something" "sees" "cat" "+")) -> ("cat" "sees" "lion" "-"))
If the lion visits the cow then the lion visits the dog.
((("lion" "visits" "cow" "+")) -> ("lion" "visits" "dog" "+"))
The lion visits the cow.
True
1
proof
[(triple12)]
("lion" "visits" "cow" "+")
triple12
The lion does not see the cow.
False
1
inv-proof
[(triple10)]
("lion" "sees" "cow" "-")
triple10
The lion visits the dog.
True
2
proof
[(((triple12) -> rule2))]
("lion" "visits" "dog" "+")
((triple12) -> (rule2 % int1))
The lion visits the dog.
("lion" "visits" "dog" "+")
int1
The lion does not visit the dog.
False
2
inv-proof
[(((triple12) -> rule2))]
("lion" "visits" "dog" "-")
((triple12) -> (rule2 % int1))
The lion visits the dog.
("lion" "visits" "dog" "+")
int1
The cat does not see the lion.
True
4
proof
[(((((triple12) -> rule2) triple9) -> rule1))]
("cat" "sees" "lion" "-")
((((triple12) -> (rule2 % int2)) triple9) -> (rule1 % int1))
The cat does not see the lion.
("cat" "sees" "lion" "-")
int1
The lion visits the dog.
("lion" "visits" "dog" "+")
int2
The cat sees the lion.
False
4
inv-proof
[(((((triple12) -> rule2) triple9) -> rule1))]
("cat" "sees" "lion" "+")
((((triple12) -> (rule2 % int2)) triple9) -> (rule1 % int1))
The cat does not see the lion.
("cat" "sees" "lion" "-")
int1
The lion visits the dog.
("lion" "visits" "dog" "+")
int2
The cow is not kind.
Unknown
inv-random
[@0: The cow is kind.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "kind" "-")
The dog is big.
Unknown
random
[@0: The dog is big.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "big" "+")
The cow does not see the dog.
Unknown
inv-random
[@0: The cow sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "dog" "-")
The dog sees the cow.
Unknown
random
[@0: The dog sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "cow" "+")
The lion does not visit the lion.
Unknown
inv-random
[@0: The lion visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "lion" "-")
The dog visits the cow.
Unknown
random
[@0: The dog visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "cow" "+")
@0: The cat eats the dog.[(triple1)] The cat is blue.[(triple2)] The cat sees the dog.[(triple3)] The cat visits the cow.[(triple4)] The cow visits the cat.[(triple5)] The dog eats the cat.[(triple6)] The dog visits the lion.[(triple7)] The lion eats the cow.[(triple8)] The lion sees the cat.[(triple9)] The lion sees the cow.[(triple10)] The lion visits the cat.[(triple11)] The lion visits the cow.[(triple12)] @1: The lion visits the dog.[(((triple12) -> rule2))] @2: The cat does not see the lion.[(((((triple12) -> rule2) triple9) -> rule1))]
The cat eats the dog.
("cat" "eats" "dog" "+")
triple1
The cat is blue.
("cat" "is" "blue" "+")
triple2
The cat sees the dog.
("cat" "sees" "dog" "+")
triple3
The cat visits the cow.
("cat" "visits" "cow" "+")
triple4
The cow visits the cat.
("cow" "visits" "cat" "+")
triple5
The dog eats the cat.
("dog" "eats" "cat" "+")
triple6
The dog visits the lion.
("dog" "visits" "lion" "+")
triple7
The lion eats the cow.
("lion" "eats" "cow" "+")
triple8
The lion sees the cat.
("lion" "sees" "cat" "+")
triple9
The lion sees the cow.
("lion" "sees" "cow" "+")
triple10
The lion visits the cat.
("lion" "visits" "cat" "+")
triple11
The lion visits the cow.
("lion" "visits" "cow" "+")
triple12
The lion visits the dog.
("lion" "visits" "dog" "+")
((triple12) -> (rule2 % int1))
The lion visits the dog.
("lion" "visits" "dog" "+")
int1
The cat does not see the lion.
("cat" "sees" "lion" "-")
((((triple12) -> (rule2 % int2)) triple9) -> (rule1 % int1))
The cat does not see the lion.
("cat" "sees" "lion" "-")
int1
The lion visits the dog.
("lion" "visits" "dog" "+")
int2