The bear sees the cat. The bear sees the dog. The bear visits the tiger. The cat is young. The cat needs the tiger. The dog does not visit the cat. The tiger is not red. The tiger needs the cat. The tiger does not see the dog. The tiger visits the cat. If something sees the tiger then the tiger visits the dog. If something visits the dog then it sees the tiger. If something sees the cat then it needs the bear. If something sees the tiger then it needs the bear. If something sees the tiger then the tiger visits the bear. If something is red then it sees the cat. If something needs the cat then the cat visits the dog. If the bear visits the dog then the bear sees the dog. If something visits the dog and it is red then it does not need the dog.
The bear sees the cat.
("bear" "sees" "cat" "+")
The bear sees the dog.
("bear" "sees" "dog" "+")
The bear visits the tiger.
("bear" "visits" "tiger" "+")
The cat is young.
("cat" "is" "young" "+")
The cat needs the tiger.
("cat" "needs" "tiger" "+")
The dog does not visit the cat.
("dog" "visits" "cat" "-")
The tiger is not red.
("tiger" "is" "red" "-")
The tiger needs the cat.
("tiger" "needs" "cat" "+")
The tiger does not see the dog.
("tiger" "sees" "dog" "-")
The tiger visits the cat.
("tiger" "visits" "cat" "+")
If something sees the tiger then the tiger visits the dog.
((("something" "sees" "tiger" "+")) -> ("tiger" "visits" "dog" "+"))
If something visits the dog then it sees the tiger.
((("something" "visits" "dog" "+")) -> ("something" "sees" "tiger" "+"))
If something sees the cat then it needs the bear.
((("something" "sees" "cat" "+")) -> ("something" "needs" "bear" "+"))
If something sees the tiger then it needs the bear.
((("something" "sees" "tiger" "+")) -> ("something" "needs" "bear" "+"))
If something sees the tiger then the tiger visits the bear.
((("something" "sees" "tiger" "+")) -> ("tiger" "visits" "bear" "+"))
If something is red then it sees the cat.
((("something" "is" "red" "+")) -> ("something" "sees" "cat" "+"))
If something needs the cat then the cat visits the dog.
((("something" "needs" "cat" "+")) -> ("cat" "visits" "dog" "+"))
If the bear visits the dog then the bear sees the dog.
((("bear" "visits" "dog" "+")) -> ("bear" "sees" "dog" "+"))
If something visits the dog and it is red then it does not need the dog.
((("something" "visits" "dog" "+") ("something" "is" "red" "+")) -> ("something" "needs" "dog" "-"))
The bear sees the dog.
True
1
proof
[(triple2)]
("bear" "sees" "dog" "+")
triple2
The tiger does not visit the cat.
False
1
inv-proof
[(triple10)]
("tiger" "visits" "cat" "-")
triple10
The bear needs the bear.
True
2
proof
[(((triple1) -> rule3))]
("bear" "needs" "bear" "+")
((triple1) -> (rule3 % int1))
The bear needs the bear.
("bear" "needs" "bear" "+")
int1
The cat does not visit the dog.
False
2
inv-proof
[(((triple8) -> rule7))]
("cat" "visits" "dog" "-")
((triple8) -> (rule7 % int1))
The cat visits the dog.
("cat" "visits" "dog" "+")
int1
The cat sees the tiger.
True
3
proof
[(((((triple8) -> rule7)) -> rule2))]
("cat" "sees" "tiger" "+")
((((triple8) -> (rule7 % int2))) -> (rule2 % int1))
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int1
The cat visits the dog.
("cat" "visits" "dog" "+")
int2
The cat does not see the tiger.
False
3
inv-proof
[(((((triple8) -> rule7)) -> rule2))]
("cat" "sees" "tiger" "-")
((((triple8) -> (rule7 % int2))) -> (rule2 % int1))
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int1
The cat visits the dog.
("cat" "visits" "dog" "+")
int2
The cat needs the bear.
True
4
proof
[(((((((triple8) -> rule7)) -> rule2)) -> rule4))]
("cat" "needs" "bear" "+")
((((((triple8) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The cat needs the bear.
("cat" "needs" "bear" "+")
int1
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int2
The cat visits the dog.
("cat" "visits" "dog" "+")
int3
The cat does not need the bear.
False
4
inv-proof
[(((((((triple8) -> rule7)) -> rule2)) -> rule4))]
("cat" "needs" "bear" "-")
((((((triple8) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The cat needs the bear.
("cat" "needs" "bear" "+")
int1
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int2
The cat visits the dog.
("cat" "visits" "dog" "+")
int3
The tiger sees the tiger.
True
5
proof
[(((((((((triple8) -> rule7)) -> rule2)) -> rule1)) -> rule2))]
("tiger" "sees" "tiger" "+")
((((((((triple8) -> (rule7 % int4))) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int2
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int3
The cat visits the dog.
("cat" "visits" "dog" "+")
int4
The tiger does not see the tiger.
False
5
inv-proof
[(((((((((triple8) -> rule7)) -> rule2)) -> rule1)) -> rule2))]
("tiger" "sees" "tiger" "-")
((((((((triple8) -> (rule7 % int4))) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int2
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int3
The cat visits the dog.
("cat" "visits" "dog" "+")
int4
The tiger needs the bear.
True
6
proof
[(((((((((((triple8) -> rule7)) -> rule2)) -> rule1)) -> rule2)) -> rule4))]
("tiger" "needs" "bear" "+")
((((((((((triple8) -> (rule7 % int5))) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The tiger needs the bear.
("tiger" "needs" "bear" "+")
int1
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int2
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int3
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int4
The cat visits the dog.
("cat" "visits" "dog" "+")
int5
The tiger does not need the bear.
False
6
inv-proof
[(((((((((((triple8) -> rule7)) -> rule2)) -> rule1)) -> rule2)) -> rule4))]
("tiger" "needs" "bear" "-")
((((((((((triple8) -> (rule7 % int5))) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The tiger needs the bear.
("tiger" "needs" "bear" "+")
int1
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int2
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int3
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int4
The cat visits the dog.
("cat" "visits" "dog" "+")
int5
The dog does not see the tiger.
Unknown
inv-rconc
[@1: The dog sees the tiger.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "sees" "tiger" "-")
The dog sees the cat.
Unknown
rconc
[@1: The dog sees the cat.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("dog" "sees" "cat" "+")
The bear does not see the tiger.
Unknown
inv-rconc
[@1: The bear sees the tiger.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "sees" "tiger" "-")
The tiger sees the cat.
Unknown
rconc
[@1: The tiger sees the cat.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("tiger" "sees" "cat" "+")
The dog does not need the bear.
Unknown
inv-rconc
[@2: The dog needs the bear.[CWA. Example of deepest failure = (rule3 <- rule6 <- FAIL)]]
("dog" "needs" "bear" "-")
The cat sees the cat.
Unknown
rconc
[@1: The cat sees the cat.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cat" "sees" "cat" "+")
The bear does not visit the dog.
Unknown
inv-random
[@0: The bear visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "dog" "-")
The bear is young.
Unknown
random
[@0: The bear is young.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "young" "+")
The cat is not blue.
Unknown
inv-random
[@0: The cat is blue.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "blue" "-")
The tiger visits the tiger.
Unknown
random
[@0: The tiger visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "tiger" "+")
The cat does not visit the tiger.
Unknown
inv-random
[@0: The cat visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "tiger" "-")
The tiger sees the bear.
Unknown
random
[@0: The tiger sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "bear" "+")
@0: The bear sees the cat.[(triple1)] The bear sees the dog.[(triple2)] The bear visits the tiger.[(triple3)] The cat is young.[(triple4)] The cat needs the tiger.[(triple5)] The dog does not visit the cat.[(triple6)] The tiger does not see the dog.[(triple9)] The tiger is not red.[(triple7)] The tiger needs the cat.[(triple8)] The tiger visits the cat.[(triple10)] @1: The bear needs the bear.[(((triple1) -> rule3))] The cat visits the dog.[(((triple8) -> rule7))] @2: The cat sees the tiger.[(((((triple8) -> rule7)) -> rule2))] @3: The cat needs the bear.[(((((((triple8) -> rule7)) -> rule2)) -> rule4))] The tiger visits the bear.[(((((((triple8) -> rule7)) -> rule2)) -> rule5) OR ((((((((((triple8) -> rule7)) -> rule2)) -> rule1)) -> rule2)) -> rule5))] The tiger visits the dog.[(((((((triple8) -> rule7)) -> rule2)) -> rule1))] @4: The tiger sees the tiger.[(((((((((triple8) -> rule7)) -> rule2)) -> rule1)) -> rule2))] @5: The tiger needs the bear.[(((((((((((triple8) -> rule7)) -> rule2)) -> rule1)) -> rule2)) -> rule4))]
The bear sees the cat.
("bear" "sees" "cat" "+")
triple1
The bear sees the dog.
("bear" "sees" "dog" "+")
triple2
The bear visits the tiger.
("bear" "visits" "tiger" "+")
triple3
The cat is young.
("cat" "is" "young" "+")
triple4
The cat needs the tiger.
("cat" "needs" "tiger" "+")
triple5
The dog does not visit the cat.
("dog" "visits" "cat" "-")
triple6
The tiger does not see the dog.
("tiger" "sees" "dog" "-")
triple9
The tiger is not red.
("tiger" "is" "red" "-")
triple7
The tiger needs the cat.
("tiger" "needs" "cat" "+")
triple8
The tiger visits the cat.
("tiger" "visits" "cat" "+")
triple10
The bear needs the bear.
("bear" "needs" "bear" "+")
((triple1) -> (rule3 % int1))
The bear needs the bear.
("bear" "needs" "bear" "+")
int1
The cat visits the dog.
("cat" "visits" "dog" "+")
((triple8) -> (rule7 % int1))
The cat visits the dog.
("cat" "visits" "dog" "+")
int1
The cat sees the tiger.
("cat" "sees" "tiger" "+")
((((triple8) -> (rule7 % int2))) -> (rule2 % int1))
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int1
The cat visits the dog.
("cat" "visits" "dog" "+")
int2
The cat needs the bear.
("cat" "needs" "bear" "+")
((((((triple8) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The cat needs the bear.
("cat" "needs" "bear" "+")
int1
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int2
The cat visits the dog.
("cat" "visits" "dog" "+")
int3
The tiger visits the bear.
("tiger" "visits" "bear" "+")
((((((triple8) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The tiger visits the bear.
("tiger" "visits" "bear" "+")
int1
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int2
The cat visits the dog.
("cat" "visits" "dog" "+")
int3
((((((((((triple8) -> (rule7 % int5))) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The tiger visits the bear.
("tiger" "visits" "bear" "+")
int1
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int2
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int3
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int4
The cat visits the dog.
("cat" "visits" "dog" "+")
int5
The tiger visits the dog.
("tiger" "visits" "dog" "+")
((((((triple8) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int1
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int2
The cat visits the dog.
("cat" "visits" "dog" "+")
int3
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
((((((((triple8) -> (rule7 % int4))) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int2
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int3
The cat visits the dog.
("cat" "visits" "dog" "+")
int4
The tiger needs the bear.
("tiger" "needs" "bear" "+")
((((((((((triple8) -> (rule7 % int5))) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The tiger needs the bear.
("tiger" "needs" "bear" "+")
int1
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int2
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int3
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int4
The cat visits the dog.
("cat" "visits" "dog" "+")
int5