The cat is big. The cat needs the lion. The cat visits the lion. The cow is cold. The cow is kind. The cow is round. The cow needs the lion. The lion is cold. The lion likes the cat. The lion likes the cow. The lion needs the cat. The rabbit is cold. The rabbit likes the cat. The rabbit needs the cat. If something needs the cat and it needs the lion then it visits the cow. If something needs the cow then the cow visits the lion. If something visits the cat then it is kind. If something visits the cat then the cat likes the cow. If something is kind then it needs the cat. If something visits the lion and it visits the cow then the lion needs the cow. If something is round and it visits the cow then it needs the cow.
The cat is big.
("cat" "is" "big" "+")
The cat needs the lion.
("cat" "needs" "lion" "+")
The cat visits the lion.
("cat" "visits" "lion" "+")
The cow is cold.
("cow" "is" "cold" "+")
The cow is kind.
("cow" "is" "kind" "+")
The cow is round.
("cow" "is" "round" "+")
The cow needs the lion.
("cow" "needs" "lion" "+")
The lion is cold.
("lion" "is" "cold" "+")
The lion likes the cat.
("lion" "likes" "cat" "+")
The lion likes the cow.
("lion" "likes" "cow" "+")
The lion needs the cat.
("lion" "needs" "cat" "+")
The rabbit is cold.
("rabbit" "is" "cold" "+")
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
If something needs the cat and it needs the lion then it visits the cow.
((("something" "needs" "cat" "+") ("something" "needs" "lion" "+")) -> ("something" "visits" "cow" "+"))
If something needs the cow then the cow visits the lion.
((("something" "needs" "cow" "+")) -> ("cow" "visits" "lion" "+"))
If something visits the cat then it is kind.
((("something" "visits" "cat" "+")) -> ("something" "is" "kind" "+"))
If something visits the cat then the cat likes the cow.
((("something" "visits" "cat" "+")) -> ("cat" "likes" "cow" "+"))
If something is kind then it needs the cat.
((("something" "is" "kind" "+")) -> ("something" "needs" "cat" "+"))
If something visits the lion and it visits the cow then the lion needs the cow.
((("something" "visits" "lion" "+") ("something" "visits" "cow" "+")) -> ("lion" "needs" "cow" "+"))
If something is round and it visits the cow then it needs the cow.
((("something" "is" "round" "+") ("something" "visits" "cow" "+")) -> ("something" "needs" "cow" "+"))
The cow needs the lion.
True
1
proof
[(triple7)]
("cow" "needs" "lion" "+")
triple7
The lion does not like the cat.
False
1
inv-proof
[(triple9)]
("lion" "likes" "cat" "-")
triple9
The cow needs the cat.
True
2
proof
[(((triple5) -> rule5))]
("cow" "needs" "cat" "+")
((triple5) -> (rule5 % int1))
The cow needs the cat.
("cow" "needs" "cat" "+")
int1
The cow does not need the cat.
False
2
inv-proof
[(((triple5) -> rule5))]
("cow" "needs" "cat" "-")
((triple5) -> (rule5 % int1))
The cow needs the cat.
("cow" "needs" "cat" "+")
int1
The cow visits the cow.
True
4
proof
[(((((triple5) -> rule5) triple7) -> rule1))]
("cow" "visits" "cow" "+")
((((triple5) -> (rule5 % int2)) triple7) -> (rule1 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
The cow needs the cat.
("cow" "needs" "cat" "+")
int2
The cow does not visit the cow.
False
4
inv-proof
[(((((triple5) -> rule5) triple7) -> rule1))]
("cow" "visits" "cow" "-")
((((triple5) -> (rule5 % int2)) triple7) -> (rule1 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
The cow needs the cat.
("cow" "needs" "cat" "+")
int2
The cow needs the cow.
True
6
proof
[(((triple6 ((((triple5) -> rule5) triple7) -> rule1)) -> rule7))]
("cow" "needs" "cow" "+")
((triple6 ((((triple5) -> (rule5 % int3)) triple7) -> (rule1 % int2))) -> (rule7 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The cow visits the cow.
("cow" "visits" "cow" "+")
int2
The cow needs the cat.
("cow" "needs" "cat" "+")
int3
The cow does not need the cow.
False
6
inv-proof
[(((triple6 ((((triple5) -> rule5) triple7) -> rule1)) -> rule7))]
("cow" "needs" "cow" "-")
((triple6 ((((triple5) -> (rule5 % int3)) triple7) -> (rule1 % int2))) -> (rule7 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The cow visits the cow.
("cow" "visits" "cow" "+")
int2
The cow needs the cat.
("cow" "needs" "cat" "+")
int3
The cow visits the lion.
True
7
proof
[(((((triple6 ((((triple5) -> rule5) triple7) -> rule1)) -> rule7)) -> rule2))]
("cow" "visits" "lion" "+")
((((triple6 ((((triple5) -> (rule5 % int4)) triple7) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
The cow visits the lion.
("cow" "visits" "lion" "+")
int1
The cow needs the cow.
("cow" "needs" "cow" "+")
int2
The cow visits the cow.
("cow" "visits" "cow" "+")
int3
The cow needs the cat.
("cow" "needs" "cat" "+")
int4
The cow does not visit the lion.
False
7
inv-proof
[(((((triple6 ((((triple5) -> rule5) triple7) -> rule1)) -> rule7)) -> rule2))]
("cow" "visits" "lion" "-")
((((triple6 ((((triple5) -> (rule5 % int4)) triple7) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
The cow visits the lion.
("cow" "visits" "lion" "+")
int1
The cow needs the cow.
("cow" "needs" "cow" "+")
int2
The cow visits the cow.
("cow" "visits" "cow" "+")
int3
The cow needs the cat.
("cow" "needs" "cat" "+")
int4
The lion needs the cow.
True
12
proof
[(((((((triple6 ((((triple5) -> rule5) triple7) -> rule1)) -> rule7)) -> rule2) ((((triple5) -> rule5) triple7) -> rule1)) -> rule6))]
("lion" "needs" "cow" "+")
((((((triple6 ((((triple5) -> (rule5 % int5)) triple7) -> (rule1 % int4))) -> (rule7 % int3))) -> (rule2 % int2)) ((((triple5) -> (rule5 % int5)) triple7) -> (rule1 % int4))) -> (rule6 % int1))
The lion needs the cow.
("lion" "needs" "cow" "+")
int1
The cow visits the lion.
("cow" "visits" "lion" "+")
int2
The cow needs the cow.
("cow" "needs" "cow" "+")
int3
The cow visits the cow.
("cow" "visits" "cow" "+")
int4
The cow needs the cat.
("cow" "needs" "cat" "+")
int5
The lion does not need the cow.
False
12
inv-proof
[(((((((triple6 ((((triple5) -> rule5) triple7) -> rule1)) -> rule7)) -> rule2) ((((triple5) -> rule5) triple7) -> rule1)) -> rule6))]
("lion" "needs" "cow" "-")
((((((triple6 ((((triple5) -> (rule5 % int5)) triple7) -> (rule1 % int4))) -> (rule7 % int3))) -> (rule2 % int2)) ((((triple5) -> (rule5 % int5)) triple7) -> (rule1 % int4))) -> (rule6 % int1))
The lion needs the cow.
("lion" "needs" "cow" "+")
int1
The cow visits the lion.
("cow" "visits" "lion" "+")
int2
The cow needs the cow.
("cow" "needs" "cow" "+")
int3
The cow visits the cow.
("cow" "visits" "cow" "+")
int4
The cow needs the cat.
("cow" "needs" "cat" "+")
int5
The cat does not like the cow.
Unknown
inv-rconc
[@1: The cat likes the cow.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cat" "likes" "cow" "-")
The cat visits the cow.
Unknown
rconc
[@3: The cat visits the cow.[CWA. Example of deepest failure = (rule1 <- rule5 <- rule3 <- FAIL)]]
("cat" "visits" "cow" "+")
The rabbit does not visit the cow.
Unknown
inv-rconc
[@1: The rabbit visits the cow.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "visits" "cow" "-")
The rabbit needs the cow.
Unknown
rconc
[@1: The rabbit needs the cow.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("rabbit" "needs" "cow" "+")
The cat is not kind.
Unknown
inv-rconc
[@1: The cat is kind.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cat" "is" "kind" "-")
The cat needs the cow.
Unknown
rconc
[@1: The cat needs the cow.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("cat" "needs" "cow" "+")
The lion does not visit the cat.
Unknown
inv-random
[@0: The lion visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "cat" "-")
The cow likes the cow.
Unknown
random
[@0: The cow likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "likes" "cow" "+")
The cat does not like the cat.
Unknown
inv-random
[@0: The cat likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "cat" "-")
The rabbit visits the cat.
Unknown
random
[@0: The rabbit visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "cat" "+")
The rabbit does not visit the rabbit.
Unknown
inv-random
[@0: The rabbit visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "rabbit" "-")
The cow visits the cat.
Unknown
random
[@0: The cow visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "cat" "+")
@0: The cat is big.[(triple1)] The cat needs the lion.[(triple2)] The cat visits the lion.[(triple3)] The cow is cold.[(triple4)] The cow is kind.[(triple5)] The cow is round.[(triple6)] The cow needs the lion.[(triple7)] The lion is cold.[(triple8)] The lion likes the cat.[(triple9)] The lion likes the cow.[(triple10)] The lion needs the cat.[(triple11)] The rabbit is cold.[(triple12)] The rabbit likes the cat.[(triple13)] The rabbit needs the cat.[(triple14)] @1: The cow needs the cat.[(((triple5) -> rule5))] @2: The cow visits the cow.[(((((triple5) -> rule5) triple7) -> rule1))] @3: The cow needs the cow.[(((triple6 ((((triple5) -> rule5) triple7) -> rule1)) -> rule7))] @4: The cow visits the lion.[(((((triple6 ((((triple5) -> rule5) triple7) -> rule1)) -> rule7)) -> rule2))] @5: The lion needs the cow.[(((((((triple6 ((((triple5) -> rule5) triple7) -> rule1)) -> rule7)) -> rule2) ((((triple5) -> rule5) triple7) -> rule1)) -> rule6))]
The cat is big.
("cat" "is" "big" "+")
triple1
The cat needs the lion.
("cat" "needs" "lion" "+")
triple2
The cat visits the lion.
("cat" "visits" "lion" "+")
triple3
The cow is cold.
("cow" "is" "cold" "+")
triple4
The cow is kind.
("cow" "is" "kind" "+")
triple5
The cow is round.
("cow" "is" "round" "+")
triple6
The cow needs the lion.
("cow" "needs" "lion" "+")
triple7
The lion is cold.
("lion" "is" "cold" "+")
triple8
The lion likes the cat.
("lion" "likes" "cat" "+")
triple9
The lion likes the cow.
("lion" "likes" "cow" "+")
triple10
The lion needs the cat.
("lion" "needs" "cat" "+")
triple11
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple12
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
triple13
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
triple14
The cow needs the cat.
("cow" "needs" "cat" "+")
((triple5) -> (rule5 % int1))
The cow needs the cat.
("cow" "needs" "cat" "+")
int1
The cow visits the cow.
("cow" "visits" "cow" "+")
((((triple5) -> (rule5 % int2)) triple7) -> (rule1 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
The cow needs the cat.
("cow" "needs" "cat" "+")
int2
The cow needs the cow.
("cow" "needs" "cow" "+")
((triple6 ((((triple5) -> (rule5 % int3)) triple7) -> (rule1 % int2))) -> (rule7 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The cow visits the cow.
("cow" "visits" "cow" "+")
int2
The cow needs the cat.
("cow" "needs" "cat" "+")
int3
The cow visits the lion.
("cow" "visits" "lion" "+")
((((triple6 ((((triple5) -> (rule5 % int4)) triple7) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
The cow visits the lion.
("cow" "visits" "lion" "+")
int1
The cow needs the cow.
("cow" "needs" "cow" "+")
int2
The cow visits the cow.
("cow" "visits" "cow" "+")
int3
The cow needs the cat.
("cow" "needs" "cat" "+")
int4
The lion needs the cow.
("lion" "needs" "cow" "+")
((((((triple6 ((((triple5) -> (rule5 % int5)) triple7) -> (rule1 % int4))) -> (rule7 % int3))) -> (rule2 % int2)) ((((triple5) -> (rule5 % int5)) triple7) -> (rule1 % int4))) -> (rule6 % int1))
The lion needs the cow.
("lion" "needs" "cow" "+")
int1
The cow visits the lion.
("cow" "visits" "lion" "+")
int2
The cow needs the cow.
("cow" "needs" "cow" "+")
int3
The cow visits the cow.
("cow" "visits" "cow" "+")
int4
The cow needs the cat.
("cow" "needs" "cat" "+")
int5