The cat is nice. The dog needs the tiger. The tiger needs the cat. If something is blue then it does not see the tiger. If something needs the dog then it needs the cat. If something sees the dog and the dog sees the tiger then the tiger is not rough. If the tiger needs the dog and the dog is nice then the tiger sees the dog. If the tiger eats the dog then the tiger is blue. If something is nice and it needs the dog then the dog needs the tiger. If something eats the dog then the dog is blue. If the tiger needs the cat then the cat eats the dog.
The cat is nice.
("cat" "is" "nice" "+")
The dog needs the tiger.
("dog" "needs" "tiger" "+")
The tiger needs the cat.
("tiger" "needs" "cat" "+")
If something is blue then it does not see the tiger.
((("something" "is" "blue" "+")) -> ("something" "sees" "tiger" "-"))
If something needs the dog then it needs the cat.
((("something" "needs" "dog" "+")) -> ("something" "needs" "cat" "+"))
If something sees the dog and the dog sees the tiger then the tiger is not rough.
((("something" "sees" "dog" "+") ("dog" "sees" "tiger" "+")) -> ("tiger" "is" "rough" "-"))
If the tiger needs the dog and the dog is nice then the tiger sees the dog.
((("tiger" "needs" "dog" "+") ("dog" "is" "nice" "+")) -> ("tiger" "sees" "dog" "+"))
If the tiger eats the dog then the tiger is blue.
((("tiger" "eats" "dog" "+")) -> ("tiger" "is" "blue" "+"))
If something is nice and it needs the dog then the dog needs the tiger.
((("something" "is" "nice" "+") ("something" "needs" "dog" "+")) -> ("dog" "needs" "tiger" "+"))
If something eats the dog then the dog is blue.
((("something" "eats" "dog" "+")) -> ("dog" "is" "blue" "+"))
If the tiger needs the cat then the cat eats the dog.
((("tiger" "needs" "cat" "+")) -> ("cat" "eats" "dog" "+"))
The tiger needs the cat.
True
1
proof
[(triple3)]
("tiger" "needs" "cat" "+")
triple3
The dog does not need the tiger.
False
1
inv-proof
[(triple2)]
("dog" "needs" "tiger" "-")
triple2
The cat eats the dog.
True
2
proof
[(((triple3) -> rule8))]
("cat" "eats" "dog" "+")
((triple3) -> (rule8 % int1))
The cat eats the dog.
("cat" "eats" "dog" "+")
int1
The cat does not eat the dog.
False
2
inv-proof
[(((triple3) -> rule8))]
("cat" "eats" "dog" "-")
((triple3) -> (rule8 % int1))
The cat eats the dog.
("cat" "eats" "dog" "+")
int1
The dog is blue.
True
3
proof
[(((((triple3) -> rule8)) -> rule7))]
("dog" "is" "blue" "+")
((((triple3) -> (rule8 % int2))) -> (rule7 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
The cat eats the dog.
("cat" "eats" "dog" "+")
int2
The dog is not blue.
False
3
inv-proof
[(((((triple3) -> rule8)) -> rule7))]
("dog" "is" "blue" "-")
((((triple3) -> (rule8 % int2))) -> (rule7 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
The cat eats the dog.
("cat" "eats" "dog" "+")
int2
The dog does not see the tiger.
True
4
proof
[(((((((triple3) -> rule8)) -> rule7)) -> rule1))]
("dog" "sees" "tiger" "-")
((((((triple3) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
The dog does not see the tiger.
("dog" "sees" "tiger" "-")
int1
The dog is blue.
("dog" "is" "blue" "+")
int2
The cat eats the dog.
("cat" "eats" "dog" "+")
int3
The dog sees the tiger.
False
4
inv-proof
[(((((((triple3) -> rule8)) -> rule7)) -> rule1))]
("dog" "sees" "tiger" "+")
((((((triple3) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
The dog does not see the tiger.
("dog" "sees" "tiger" "-")
int1
The dog is blue.
("dog" "is" "blue" "+")
int2
The cat eats the dog.
("cat" "eats" "dog" "+")
int3
The cat does not need the cat.
Unknown
inv-rconc
[@1: The cat needs the cat.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "needs" "cat" "-")
The tiger is blue.
Unknown
rconc
[@1: The tiger is blue.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("tiger" "is" "blue" "+")
The tiger does not see the dog.
Unknown
inv-rconc
[@1: The tiger sees the dog.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("tiger" "sees" "dog" "-")
The dog needs the cat.
Unknown
rconc
[@1: The dog needs the cat.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "needs" "cat" "+")
The tiger does not need the tiger.
Unknown
inv-random
[@0: The tiger needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "tiger" "-")
The dog sees the dog.
Unknown
random
[@0: The dog sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "dog" "+")
The cat does not eat the tiger.
Unknown
inv-random
[@0: The cat eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "tiger" "-")
The dog is rough.
Unknown
random
[@0: The dog is rough.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "rough" "+")
@0: The cat is nice.[(triple1)] The dog needs the tiger.[(triple2)] The tiger needs the cat.[(triple3)] @1: The cat eats the dog.[(((triple3) -> rule8))] @2: The dog is blue.[(((((triple3) -> rule8)) -> rule7))] @3: The dog does not see the tiger.[(((((((triple3) -> rule8)) -> rule7)) -> rule1))]
The cat is nice.
("cat" "is" "nice" "+")
triple1
The dog needs the tiger.
("dog" "needs" "tiger" "+")
triple2
The tiger needs the cat.
("tiger" "needs" "cat" "+")
triple3
The cat eats the dog.
("cat" "eats" "dog" "+")
((triple3) -> (rule8 % int1))
The cat eats the dog.
("cat" "eats" "dog" "+")
int1
The dog is blue.
("dog" "is" "blue" "+")
((((triple3) -> (rule8 % int2))) -> (rule7 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
The cat eats the dog.
("cat" "eats" "dog" "+")
int2
The dog does not see the tiger.
("dog" "sees" "tiger" "-")
((((((triple3) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
The dog does not see the tiger.
("dog" "sees" "tiger" "-")
int1
The dog is blue.
("dog" "is" "blue" "+")
int2
The cat eats the dog.
("cat" "eats" "dog" "+")
int3