The dog needs the tiger. The lion needs the dog. The tiger needs the dog. If someone is green then they are rough. If someone needs the tiger and they eat the tiger then they are green. If someone needs the lion then they are rough. All green people are nice. If someone is rough and green then they need the tiger. If someone is blue then they need the lion. If the tiger needs the dog then the dog eats the tiger. If someone is young then they eat the lion.
The dog needs the tiger.
("dog" "needs" "tiger" "+")
The lion needs the dog.
("lion" "needs" "dog" "+")
The tiger needs the dog.
("tiger" "needs" "dog" "+")
If someone is green then they are rough.
((("someone" "is" "green" "+")) -> ("someone" "is" "rough" "+"))
If someone needs the tiger and they eat the tiger then they are green.
((("someone" "needs" "tiger" "+") ("someone" "eats" "tiger" "+")) -> ("someone" "is" "green" "+"))
If someone needs the lion then they are rough.
((("someone" "needs" "lion" "+")) -> ("someone" "is" "rough" "+"))
All green people are nice.
((("someone" "is" "green" "+")) -> ("someone" "is" "nice" "+"))
If someone is rough and green then they need the tiger.
((("someone" "is" "rough" "+") ("someone" "is" "green" "+")) -> ("someone" "needs" "tiger" "+"))
If someone is blue then they need the lion.
((("someone" "is" "blue" "+")) -> ("someone" "needs" "lion" "+"))
If the tiger needs the dog then the dog eats the tiger.
((("tiger" "needs" "dog" "+")) -> ("dog" "eats" "tiger" "+"))
If someone is young then they eat the lion.
((("someone" "is" "young" "+")) -> ("someone" "eats" "lion" "+"))
The tiger needs the dog.
True
1
proof
[(triple3)]
("tiger" "needs" "dog" "+")
triple3
The dog does not need the tiger.
False
1
inv-proof
[(triple1)]
("dog" "needs" "tiger" "-")
triple1
The dog eats the tiger.
True
2
proof
[(((triple3) -> rule7))]
("dog" "eats" "tiger" "+")
((triple3) -> (rule7 % int1))
The dog eats the tiger.
("dog" "eats" "tiger" "+")
int1
The dog does not eat the tiger.
False
2
inv-proof
[(((triple3) -> rule7))]
("dog" "eats" "tiger" "-")
((triple3) -> (rule7 % int1))
The dog eats the tiger.
("dog" "eats" "tiger" "+")
int1
The dog is green.
True
4
proof
[(((triple1 ((triple3) -> rule7)) -> rule2))]
("dog" "is" "green" "+")
((triple1 ((triple3) -> (rule7 % int2))) -> (rule2 % int1))
The dog is green.
("dog" "is" "green" "+")
int1
The dog eats the tiger.
("dog" "eats" "tiger" "+")
int2
The dog is not green.
False
4
inv-proof
[(((triple1 ((triple3) -> rule7)) -> rule2))]
("dog" "is" "green" "-")
((triple1 ((triple3) -> (rule7 % int2))) -> (rule2 % int1))
The dog is green.
("dog" "is" "green" "+")
int1
The dog eats the tiger.
("dog" "eats" "tiger" "+")
int2
The dog is rough.
True
5
proof
[(((((triple1 ((triple3) -> rule7)) -> rule2)) -> rule1))]
("dog" "is" "rough" "+")
((((triple1 ((triple3) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The dog is green.
("dog" "is" "green" "+")
int2
The dog eats the tiger.
("dog" "eats" "tiger" "+")
int3
The dog is not rough.
False
5
inv-proof
[(((((triple1 ((triple3) -> rule7)) -> rule2)) -> rule1))]
("dog" "is" "rough" "-")
((((triple1 ((triple3) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The dog is green.
("dog" "is" "green" "+")
int2
The dog eats the tiger.
("dog" "eats" "tiger" "+")
int3
The lion does not eat the lion.
Unknown
inv-rconc
[@1: The lion eats the lion.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("lion" "eats" "lion" "-")
The tiger needs the tiger.
Unknown
rconc
[@2: The tiger needs the tiger.[CWA. Example of deepest failure = (rule5 <- rule2 <- FAIL)]]
("tiger" "needs" "tiger" "+")
The dog does not need the lion.
Unknown
inv-rconc
[@1: The dog needs the lion.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("dog" "needs" "lion" "-")
The tiger is rough.
Unknown
rconc
[@2: The tiger is rough.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("tiger" "is" "rough" "+")
The lion is not young.
Unknown
inv-random
[@0: The lion is young.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "young" "-")
The dog is young.
Unknown
random
[@0: The dog is young.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "young" "+")
The tiger does not eat the tiger.
Unknown
inv-random
[@0: The tiger eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "tiger" "-")
The lion chases the tiger.
Unknown
random
[@0: The lion chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "tiger" "+")
@0: The dog needs the tiger.[(triple1)] The lion needs the dog.[(triple2)] The tiger needs the dog.[(triple3)] @1: The dog eats the tiger.[(((triple3) -> rule7))] @2: The dog is green.[(((triple1 ((triple3) -> rule7)) -> rule2))] @3: The dog is nice.[(((((triple1 ((triple3) -> rule7)) -> rule2)) -> rule4))] The dog is rough.[(((((triple1 ((triple3) -> rule7)) -> rule2)) -> rule1))]
The dog needs the tiger.
("dog" "needs" "tiger" "+")
triple1
The lion needs the dog.
("lion" "needs" "dog" "+")
triple2
The tiger needs the dog.
("tiger" "needs" "dog" "+")
triple3
The dog eats the tiger.
("dog" "eats" "tiger" "+")
((triple3) -> (rule7 % int1))
The dog eats the tiger.
("dog" "eats" "tiger" "+")
int1
The dog is green.
("dog" "is" "green" "+")
((triple1 ((triple3) -> (rule7 % int2))) -> (rule2 % int1))
The dog is green.
("dog" "is" "green" "+")
int1
The dog eats the tiger.
("dog" "eats" "tiger" "+")
int2
The dog is nice.
("dog" "is" "nice" "+")
((((triple1 ((triple3) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The dog is nice.
("dog" "is" "nice" "+")
int1
The dog is green.
("dog" "is" "green" "+")
int2
The dog eats the tiger.
("dog" "eats" "tiger" "+")
int3
The dog is rough.
("dog" "is" "rough" "+")
((((triple1 ((triple3) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The dog is green.
("dog" "is" "green" "+")
int2
The dog eats the tiger.
("dog" "eats" "tiger" "+")
int3