The cat is nice. The cat sees the dog. The cow likes the cat. The cow visits the dog. The dog is green. The dog is red. The dog likes the lion. The dog sees the cat. The dog sees the cow. The dog sees the lion. The lion sees the cat. If the lion likes the dog and the dog visits the cat then the dog visits the lion. If someone visits the cat then the cat visits the cow. If someone visits the cow then they visit the cat. If someone visits the dog then they like the dog. If the lion likes the cat then the cat likes the cow. If someone likes the dog then they like the cow. If someone is red then they are nice. If someone likes the dog and the dog sees the cow then the dog visits the cow. If someone visits the cow then they see the dog.
The cat is nice.
("cat" "is" "nice" "+")
The cat sees the dog.
("cat" "sees" "dog" "+")
The cow likes the cat.
("cow" "likes" "cat" "+")
The cow visits the dog.
("cow" "visits" "dog" "+")
The dog is green.
("dog" "is" "green" "+")
The dog is red.
("dog" "is" "red" "+")
The dog likes the lion.
("dog" "likes" "lion" "+")
The dog sees the cat.
("dog" "sees" "cat" "+")
The dog sees the cow.
("dog" "sees" "cow" "+")
The dog sees the lion.
("dog" "sees" "lion" "+")
The lion sees the cat.
("lion" "sees" "cat" "+")
If the lion likes the dog and the dog visits the cat then the dog visits the lion.
((("lion" "likes" "dog" "+") ("dog" "visits" "cat" "+")) -> ("dog" "visits" "lion" "+"))
If someone visits the cat then the cat visits the cow.
((("someone" "visits" "cat" "+")) -> ("cat" "visits" "cow" "+"))
If someone visits the cow then they visit the cat.
((("someone" "visits" "cow" "+")) -> ("someone" "visits" "cat" "+"))
If someone visits the dog then they like the dog.
((("someone" "visits" "dog" "+")) -> ("someone" "likes" "dog" "+"))
If the lion likes the cat then the cat likes the cow.
((("lion" "likes" "cat" "+")) -> ("cat" "likes" "cow" "+"))
If someone likes the dog then they like the cow.
((("someone" "likes" "dog" "+")) -> ("someone" "likes" "cow" "+"))
If someone is red then they are nice.
((("someone" "is" "red" "+")) -> ("someone" "is" "nice" "+"))
If someone likes the dog and the dog sees the cow then the dog visits the cow.
((("someone" "likes" "dog" "+") ("dog" "sees" "cow" "+")) -> ("dog" "visits" "cow" "+"))
If someone visits the cow then they see the dog.
((("someone" "visits" "cow" "+")) -> ("someone" "sees" "dog" "+"))
The cat sees the dog.
True
1
proof
[(triple2 OR ((((((((((triple4) -> rule4) triple9) -> rule8)) -> rule3)) -> rule2)) -> rule9))]
("cat" "sees" "dog" "+")
triple2
((((((((((triple4) -> (rule4 % int5)) triple9) -> (rule8 % int4))) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule9 % int1))
The cat sees the dog.
("cat" "sees" "dog" "+")
int1
The cat visits the cow.
("cat" "visits" "cow" "+")
int2
The dog visits the cat.
("dog" "visits" "cat" "+")
int3
The dog visits the cow.
("dog" "visits" "cow" "+")
int4
The cow likes the dog.
("cow" "likes" "dog" "+")
int5
The dog does not see the cat.
False
1
inv-proof
[(triple8)]
("dog" "sees" "cat" "-")
triple8
The dog is nice.
True
2
proof
[(((triple6) -> rule7))]
("dog" "is" "nice" "+")
((triple6) -> (rule7 % int1))
The dog is nice.
("dog" "is" "nice" "+")
int1
The dog is not nice.
False
2
inv-proof
[(((triple6) -> rule7))]
("dog" "is" "nice" "-")
((triple6) -> (rule7 % int1))
The dog is nice.
("dog" "is" "nice" "+")
int1
The cow likes the cow.
True
3
proof
[(((((triple4) -> rule4)) -> rule6))]
("cow" "likes" "cow" "+")
((((triple4) -> (rule4 % int2))) -> (rule6 % int1))
The cow likes the cow.
("cow" "likes" "cow" "+")
int1
The cow likes the dog.
("cow" "likes" "dog" "+")
int2
The cow does not like the cow.
False
3
inv-proof
[(((((triple4) -> rule4)) -> rule6))]
("cow" "likes" "cow" "-")
((((triple4) -> (rule4 % int2))) -> (rule6 % int1))
The cow likes the cow.
("cow" "likes" "cow" "+")
int1
The cow likes the dog.
("cow" "likes" "dog" "+")
int2
The dog visits the cat.
True
5
proof
[(((((((triple4) -> rule4) triple9) -> rule8)) -> rule3))]
("dog" "visits" "cat" "+")
((((((triple4) -> (rule4 % int3)) triple9) -> (rule8 % int2))) -> (rule3 % int1))
The dog visits the cat.
("dog" "visits" "cat" "+")
int1
The dog visits the cow.
("dog" "visits" "cow" "+")
int2
The cow likes the dog.
("cow" "likes" "dog" "+")
int3
The dog does not see the dog.
False
5
inv-proof
[(((((((triple4) -> rule4) triple9) -> rule8)) -> rule9))]
("dog" "sees" "dog" "-")
((((((triple4) -> (rule4 % int3)) triple9) -> (rule8 % int2))) -> (rule9 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
The dog visits the cow.
("dog" "visits" "cow" "+")
int2
The cow likes the dog.
("cow" "likes" "dog" "+")
int3
The cat visits the cow.
True
6
proof
[(((((((((triple4) -> rule4) triple9) -> rule8)) -> rule3)) -> rule2))]
("cat" "visits" "cow" "+")
((((((((triple4) -> (rule4 % int4)) triple9) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The cat visits the cow.
("cat" "visits" "cow" "+")
int1
The dog visits the cat.
("dog" "visits" "cat" "+")
int2
The dog visits the cow.
("dog" "visits" "cow" "+")
int3
The cow likes the dog.
("cow" "likes" "dog" "+")
int4
The cat does not visit the cow.
False
6
inv-proof
[(((((((((triple4) -> rule4) triple9) -> rule8)) -> rule3)) -> rule2))]
("cat" "visits" "cow" "-")
((((((((triple4) -> (rule4 % int4)) triple9) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The cat visits the cow.
("cat" "visits" "cow" "+")
int1
The dog visits the cat.
("dog" "visits" "cat" "+")
int2
The dog visits the cow.
("dog" "visits" "cow" "+")
int3
The cow likes the dog.
("cow" "likes" "dog" "+")
int4
The cat visits the cat.
True
7
proof
[(((((((((((triple4) -> rule4) triple9) -> rule8)) -> rule3)) -> rule2)) -> rule3))]
("cat" "visits" "cat" "+")
((((((((((triple4) -> (rule4 % int5)) triple9) -> (rule8 % int4))) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The cat visits the cow.
("cat" "visits" "cow" "+")
int2
The dog visits the cat.
("dog" "visits" "cat" "+")
int3
The dog visits the cow.
("dog" "visits" "cow" "+")
int4
The cow likes the dog.
("cow" "likes" "dog" "+")
int5
The cat does not visit the cat.
False
7
inv-proof
[(((((((((((triple4) -> rule4) triple9) -> rule8)) -> rule3)) -> rule2)) -> rule3))]
("cat" "visits" "cat" "-")
((((((((((triple4) -> (rule4 % int5)) triple9) -> (rule8 % int4))) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The cat visits the cow.
("cat" "visits" "cow" "+")
int2
The dog visits the cat.
("dog" "visits" "cat" "+")
int3
The dog visits the cow.
("dog" "visits" "cow" "+")
int4
The cow likes the dog.
("cow" "likes" "dog" "+")
int5
The dog does not like the dog.
Unknown
inv-rconc
[@1: The dog likes the dog.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("dog" "likes" "dog" "-")
The lion likes the dog.
Unknown
rconc
[@1: The lion likes the dog.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("lion" "likes" "dog" "+")
The cow does not see the dog.
Unknown
inv-rconc
[@1: The cow sees the dog.[CWA. Example of deepest failure = (rule9 <- FAIL)]]
("cow" "sees" "dog" "-")
The dog visits the lion.
Unknown
rconc
[@2: The dog visits the lion.[CWA. Example of deepest failure = (rule1 <- rule4 <- FAIL)]]
("dog" "visits" "lion" "+")
The cat does not like the cow.
Unknown
inv-rconc
[@2: The cat likes the cow.[CWA. Example of deepest failure = (rule6 <- rule4 <- FAIL)]]
("cat" "likes" "cow" "-")
The cow visits the cat.
Unknown
rconc
[@1: The cow visits the cat.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cow" "visits" "cat" "+")
The dog is not cold.
Unknown
inv-random
[@0: The dog is cold.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "cold" "-")
The cat visits the lion.
Unknown
random
[@0: The cat visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "lion" "+")
The cat is not cold.
Unknown
inv-random
[@0: The cat is cold.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "cold" "-")
The cow sees the cat.
Unknown
random
[@0: The cow sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "cat" "+")
The cow does not visit the cow.
Unknown
inv-random
[@0: The cow visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "cow" "-")
The lion visits the dog.
Unknown
random
[@0: The lion visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "dog" "+")
@0: The cat is nice.[(triple1)] The cat sees the dog.[(triple2 OR ((((((((((triple4) -> rule4) triple9) -> rule8)) -> rule3)) -> rule2)) -> rule9))] The cow likes the cat.[(triple3)] The cow visits the dog.[(triple4)] The dog is green.[(triple5)] The dog is red.[(triple6)] The dog likes the lion.[(triple7)] The dog sees the cat.[(triple8)] The dog sees the cow.[(triple9)] The dog sees the lion.[(triple10)] The lion sees the cat.[(triple11)] @1: The cow likes the dog.[(((triple4) -> rule4))] The dog is nice.[(((triple6) -> rule7))] @2: The cow likes the cow.[(((((triple4) -> rule4)) -> rule6))] The dog visits the cow.[(((((triple4) -> rule4) triple9) -> rule8))] @3: The dog sees the dog.[(((((((triple4) -> rule4) triple9) -> rule8)) -> rule9))] The dog visits the cat.[(((((((triple4) -> rule4) triple9) -> rule8)) -> rule3))] @4: The cat visits the cow.[(((((((((triple4) -> rule4) triple9) -> rule8)) -> rule3)) -> rule2))] @5: The cat visits the cat.[(((((((((((triple4) -> rule4) triple9) -> rule8)) -> rule3)) -> rule2)) -> rule3))]
The cat is nice.
("cat" "is" "nice" "+")
triple1
The cat sees the dog.
("cat" "sees" "dog" "+")
triple2
((((((((((triple4) -> (rule4 % int5)) triple9) -> (rule8 % int4))) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule9 % int1))
The cat sees the dog.
("cat" "sees" "dog" "+")
int1
The cat visits the cow.
("cat" "visits" "cow" "+")
int2
The dog visits the cat.
("dog" "visits" "cat" "+")
int3
The dog visits the cow.
("dog" "visits" "cow" "+")
int4
The cow likes the dog.
("cow" "likes" "dog" "+")
int5
The cow likes the cat.
("cow" "likes" "cat" "+")
triple3
The cow visits the dog.
("cow" "visits" "dog" "+")
triple4
The dog is green.
("dog" "is" "green" "+")
triple5
The dog is red.
("dog" "is" "red" "+")
triple6
The dog likes the lion.
("dog" "likes" "lion" "+")
triple7
The dog sees the cat.
("dog" "sees" "cat" "+")
triple8
The dog sees the cow.
("dog" "sees" "cow" "+")
triple9
The dog sees the lion.
("dog" "sees" "lion" "+")
triple10
The lion sees the cat.
("lion" "sees" "cat" "+")
triple11
The cow likes the dog.
("cow" "likes" "dog" "+")
((triple4) -> (rule4 % int1))
The cow likes the dog.
("cow" "likes" "dog" "+")
int1
The dog is nice.
("dog" "is" "nice" "+")
((triple6) -> (rule7 % int1))
The dog is nice.
("dog" "is" "nice" "+")
int1
The cow likes the cow.
("cow" "likes" "cow" "+")
((((triple4) -> (rule4 % int2))) -> (rule6 % int1))
The cow likes the cow.
("cow" "likes" "cow" "+")
int1
The cow likes the dog.
("cow" "likes" "dog" "+")
int2
The dog visits the cow.
("dog" "visits" "cow" "+")
((((triple4) -> (rule4 % int2)) triple9) -> (rule8 % int1))
The dog visits the cow.
("dog" "visits" "cow" "+")
int1
The cow likes the dog.
("cow" "likes" "dog" "+")
int2
The dog sees the dog.
("dog" "sees" "dog" "+")
((((((triple4) -> (rule4 % int3)) triple9) -> (rule8 % int2))) -> (rule9 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
The dog visits the cow.
("dog" "visits" "cow" "+")
int2
The cow likes the dog.
("cow" "likes" "dog" "+")
int3
The dog visits the cat.
("dog" "visits" "cat" "+")
((((((triple4) -> (rule4 % int3)) triple9) -> (rule8 % int2))) -> (rule3 % int1))
The dog visits the cat.
("dog" "visits" "cat" "+")
int1
The dog visits the cow.
("dog" "visits" "cow" "+")
int2
The cow likes the dog.
("cow" "likes" "dog" "+")
int3
The cat visits the cow.
("cat" "visits" "cow" "+")
((((((((triple4) -> (rule4 % int4)) triple9) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The cat visits the cow.
("cat" "visits" "cow" "+")
int1
The dog visits the cat.
("dog" "visits" "cat" "+")
int2
The dog visits the cow.
("dog" "visits" "cow" "+")
int3
The cow likes the dog.
("cow" "likes" "dog" "+")
int4
The cat visits the cat.
("cat" "visits" "cat" "+")
((((((((((triple4) -> (rule4 % int5)) triple9) -> (rule8 % int4))) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The cat visits the cow.
("cat" "visits" "cow" "+")
int2
The dog visits the cat.
("dog" "visits" "cat" "+")
int3
The dog visits the cow.
("dog" "visits" "cow" "+")
int4
The cow likes the dog.
("cow" "likes" "dog" "+")
int5