The cat chases the dog. The cat is nice. The cat is young. The cat needs the tiger. The dog chases the cat. The dog does not chase the lion. The dog is nice. The dog is not red. The lion is red. The lion is not young. The lion needs the cat. The lion visits the cat. The lion visits the dog. The tiger needs the lion. If something visits the dog then it needs the cat. If the tiger chases the lion and the tiger visits the dog then the dog is not red. If something visits the dog and it is not nice then it needs the lion. If something is nice and it does not chase the cat then the cat visits the lion. If the cat is kind then the cat visits the tiger. All young things are kind. If something visits the tiger then it visits the dog. If something needs the cat then it does not visit the lion.
The cat chases the dog.
("cat" "chases" "dog" "+")
The cat is nice.
("cat" "is" "nice" "+")
The cat is young.
("cat" "is" "young" "+")
The cat needs the tiger.
("cat" "needs" "tiger" "+")
The dog chases the cat.
("dog" "chases" "cat" "+")
The dog does not chase the lion.
("dog" "chases" "lion" "-")
The dog is nice.
("dog" "is" "nice" "+")
The dog is not red.
("dog" "is" "red" "-")
The lion is red.
("lion" "is" "red" "+")
The lion is not young.
("lion" "is" "young" "-")
The lion needs the cat.
("lion" "needs" "cat" "+")
The lion visits the cat.
("lion" "visits" "cat" "+")
The lion visits the dog.
("lion" "visits" "dog" "+")
The tiger needs the lion.
("tiger" "needs" "lion" "+")
If something visits the dog then it needs the cat.
((("something" "visits" "dog" "+")) -> ("something" "needs" "cat" "+"))
If the tiger chases the lion and the tiger visits the dog then the dog is not red.
((("tiger" "chases" "lion" "+") ("tiger" "visits" "dog" "+")) -> ("dog" "is" "red" "-"))
If something visits the dog and it is not nice then it needs the lion.
((("something" "visits" "dog" "+") ("something" "is" "nice" "~")) -> ("something" "needs" "lion" "+"))
If something is nice and it does not chase the cat then the cat visits the lion.
((("something" "is" "nice" "+") ("something" "chases" "cat" "~")) -> ("cat" "visits" "lion" "+"))
If the cat is kind then the cat visits the tiger.
((("cat" "is" "kind" "+")) -> ("cat" "visits" "tiger" "+"))
All young things are kind.
((("something" "is" "young" "+")) -> ("something" "is" "kind" "+"))
If something visits the tiger then it visits the dog.
((("something" "visits" "tiger" "+")) -> ("something" "visits" "dog" "+"))
If something needs the cat then it does not visit the lion.
((("something" "needs" "cat" "+")) -> ("something" "visits" "lion" "-"))
The tiger needs the lion.
True
1
proof
[(triple14)]
("tiger" "needs" "lion" "+")
triple14
The cat is not nice.
False
1
inv-proof
[(triple2)]
("cat" "is" "nice" "-")
triple2
The cat is kind.
True
2
proof
[(((triple3) -> rule6))]
("cat" "is" "kind" "+")
((triple3) -> (rule6 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The lion visits the lion.
False
2
inv-proof
[(((triple11) -> rule8) OR ((((triple13) -> rule1)) -> rule8))]
("lion" "visits" "lion" "+")
((triple11) -> (rule8 % int1))
The lion does not visit the lion.
("lion" "visits" "lion" "-")
int1
((((triple13) -> (rule1 % int2))) -> (rule8 % int1))
The lion does not visit the lion.
("lion" "visits" "lion" "-")
int1
The lion needs the cat.
("lion" "needs" "cat" "+")
int2
The cat visits the tiger.
True
3
proof
[(((((triple3) -> rule6)) -> rule5))]
("cat" "visits" "tiger" "+")
((((triple3) -> (rule6 % int2))) -> (rule5 % int1))
The cat visits the tiger.
("cat" "visits" "tiger" "+")
int1
The cat is kind.
("cat" "is" "kind" "+")
int2
The cat does not visit the tiger.
False
3
inv-proof
[(((((triple3) -> rule6)) -> rule5))]
("cat" "visits" "tiger" "-")
((((triple3) -> (rule6 % int2))) -> (rule5 % int1))
The cat visits the tiger.
("cat" "visits" "tiger" "+")
int1
The cat is kind.
("cat" "is" "kind" "+")
int2
The cat visits the dog.
True
4
proof
[(((((((triple3) -> rule6)) -> rule5)) -> rule7))]
("cat" "visits" "dog" "+")
((((((triple3) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
The cat visits the dog.
("cat" "visits" "dog" "+")
int1
The cat visits the tiger.
("cat" "visits" "tiger" "+")
int2
The cat is kind.
("cat" "is" "kind" "+")
int3
The cat does not visit the dog.
False
4
inv-proof
[(((((((triple3) -> rule6)) -> rule5)) -> rule7))]
("cat" "visits" "dog" "-")
((((((triple3) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
The cat visits the dog.
("cat" "visits" "dog" "+")
int1
The cat visits the tiger.
("cat" "visits" "tiger" "+")
int2
The cat is kind.
("cat" "is" "kind" "+")
int3
The cat needs the cat.
True
5
proof
[(((((((((triple3) -> rule6)) -> rule5)) -> rule7)) -> rule1))]
("cat" "needs" "cat" "+")
((((((((triple3) -> (rule6 % int4))) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The cat visits the dog.
("cat" "visits" "dog" "+")
int2
The cat visits the tiger.
("cat" "visits" "tiger" "+")
int3
The cat is kind.
("cat" "is" "kind" "+")
int4
The cat does not need the cat.
False
5
inv-proof
[(((((((((triple3) -> rule6)) -> rule5)) -> rule7)) -> rule1))]
("cat" "needs" "cat" "-")
((((((((triple3) -> (rule6 % int4))) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The cat visits the dog.
("cat" "visits" "dog" "+")
int2
The cat visits the tiger.
("cat" "visits" "tiger" "+")
int3
The cat is kind.
("cat" "is" "kind" "+")
int4
The cat does not visit the lion.
True
6
proof
[(((((((((((triple3) -> rule6)) -> rule5)) -> rule7)) -> rule1)) -> rule8))]
("cat" "visits" "lion" "-")
((((((((((triple3) -> (rule6 % int5))) -> (rule5 % int4))) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
The cat does not visit the lion.
("cat" "visits" "lion" "-")
int1
The cat needs the cat.
("cat" "needs" "cat" "+")
int2
The cat visits the dog.
("cat" "visits" "dog" "+")
int3
The cat visits the tiger.
("cat" "visits" "tiger" "+")
int4
The cat is kind.
("cat" "is" "kind" "+")
int5
The cat visits the lion.
False
6
inv-proof
[(((((((((((triple3) -> rule6)) -> rule5)) -> rule7)) -> rule1)) -> rule8))]
("cat" "visits" "lion" "+")
((((((((((triple3) -> (rule6 % int5))) -> (rule5 % int4))) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
The cat does not visit the lion.
("cat" "visits" "lion" "-")
int1
The cat needs the cat.
("cat" "needs" "cat" "+")
int2
The cat visits the dog.
("cat" "visits" "dog" "+")
int3
The cat visits the tiger.
("cat" "visits" "tiger" "+")
int4
The cat is kind.
("cat" "is" "kind" "+")
int5
The dog does not visit the dog.
Unknown
inv-rconc
[@1: The dog visits the dog.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("dog" "visits" "dog" "-")
The tiger needs the cat.
Unknown
rconc
[@2: The tiger needs the cat.[CWA. Example of deepest failure = (rule1 <- rule7 <- FAIL)]]
("tiger" "needs" "cat" "+")
The dog does not need the lion.
Unknown
inv-rconc
[@1: The dog needs the lion.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("dog" "needs" "lion" "-")
The lion needs the lion.
Unknown
rconc
[@1: The lion needs the lion.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("lion" "needs" "lion" "+")
The cat does not need the lion.
Unknown
inv-rconc
[@1: The cat needs the lion.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cat" "needs" "lion" "-")
The dog needs the cat.
Unknown
rconc
[@2: The dog needs the cat.[CWA. Example of deepest failure = (rule1 <- rule7 <- FAIL)]]
("dog" "needs" "cat" "+")
The cat does not need the dog.
Unknown
inv-random
[@0: The cat needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "dog" "-")
The dog is young.
Unknown
random
[@0: The dog is young.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "young" "+")
The tiger does not visit the cat.
Unknown
inv-random
[@0: The tiger visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "cat" "-")
The dog needs the tiger.
Unknown
random
[@0: The dog needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "tiger" "+")
The cat does not chase the tiger.
Unknown
inv-random
[@0: The cat chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "tiger" "-")
The dog visits the lion.
Unknown
random
[@0: The dog visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "lion" "+")
@0: The cat chases the dog.[(triple1)] The cat is nice.[(triple2)] The cat is young.[(triple3)] The cat needs the tiger.[(triple4)] The dog chases the cat.[(triple5)] The dog does not chase the lion.[(triple6)] The dog is nice.[(triple7)] The dog is not red.[(triple8)] The lion is not young.[(triple10)] The lion is red.[(triple9)] The lion needs the cat.[(triple11 OR ((triple13) -> rule1))] The lion visits the cat.[(triple12)] The lion visits the dog.[(triple13)] The tiger needs the lion.[(triple14)] @1: The cat is kind.[(((triple3) -> rule6))] The lion does not visit the lion.[(((triple11) -> rule8) OR ((((triple13) -> rule1)) -> rule8))] @2: The cat visits the tiger.[(((((triple3) -> rule6)) -> rule5))] @3: The cat visits the dog.[(((((((triple3) -> rule6)) -> rule5)) -> rule7))] @4: The cat needs the cat.[(((((((((triple3) -> rule6)) -> rule5)) -> rule7)) -> rule1))] @5: The cat does not visit the lion.[(((((((((((triple3) -> rule6)) -> rule5)) -> rule7)) -> rule1)) -> rule8))]
The cat chases the dog.
("cat" "chases" "dog" "+")
triple1
The cat is nice.
("cat" "is" "nice" "+")
triple2
The cat is young.
("cat" "is" "young" "+")
triple3
The cat needs the tiger.
("cat" "needs" "tiger" "+")
triple4
The dog chases the cat.
("dog" "chases" "cat" "+")
triple5
The dog does not chase the lion.
("dog" "chases" "lion" "-")
triple6
The dog is nice.
("dog" "is" "nice" "+")
triple7
The dog is not red.
("dog" "is" "red" "-")
triple8
The lion is not young.
("lion" "is" "young" "-")
triple10
The lion is red.
("lion" "is" "red" "+")
triple9
The lion needs the cat.
("lion" "needs" "cat" "+")
triple11
((triple13) -> (rule1 % int1))
The lion needs the cat.
("lion" "needs" "cat" "+")
int1
The lion visits the cat.
("lion" "visits" "cat" "+")
triple12
The lion visits the dog.
("lion" "visits" "dog" "+")
triple13
The tiger needs the lion.
("tiger" "needs" "lion" "+")
triple14
The cat is kind.
("cat" "is" "kind" "+")
((triple3) -> (rule6 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The lion does not visit the lion.
("lion" "visits" "lion" "-")
((triple11) -> (rule8 % int1))
The lion does not visit the lion.
("lion" "visits" "lion" "-")
int1
((((triple13) -> (rule1 % int2))) -> (rule8 % int1))
The lion does not visit the lion.
("lion" "visits" "lion" "-")
int1
The lion needs the cat.
("lion" "needs" "cat" "+")
int2
The cat visits the tiger.
("cat" "visits" "tiger" "+")
((((triple3) -> (rule6 % int2))) -> (rule5 % int1))
The cat visits the tiger.
("cat" "visits" "tiger" "+")
int1
The cat is kind.
("cat" "is" "kind" "+")
int2
The cat visits the dog.
("cat" "visits" "dog" "+")
((((((triple3) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
The cat visits the dog.
("cat" "visits" "dog" "+")
int1
The cat visits the tiger.
("cat" "visits" "tiger" "+")
int2
The cat is kind.
("cat" "is" "kind" "+")
int3
The cat needs the cat.
("cat" "needs" "cat" "+")
((((((((triple3) -> (rule6 % int4))) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The cat visits the dog.
("cat" "visits" "dog" "+")
int2
The cat visits the tiger.
("cat" "visits" "tiger" "+")
int3
The cat is kind.
("cat" "is" "kind" "+")
int4
The cat does not visit the lion.
("cat" "visits" "lion" "-")
((((((((((triple3) -> (rule6 % int5))) -> (rule5 % int4))) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
The cat does not visit the lion.
("cat" "visits" "lion" "-")
int1
The cat needs the cat.
("cat" "needs" "cat" "+")
int2
The cat visits the dog.
("cat" "visits" "dog" "+")
int3
The cat visits the tiger.
("cat" "visits" "tiger" "+")
int4
The cat is kind.
("cat" "is" "kind" "+")
int5