The dog visits the tiger. The tiger visits the dog. If something needs the dog then it is round. If something is blue and it needs the tiger then it is round. If something likes the tiger then it visits the tiger. If the dog likes the tiger and the tiger needs the dog then the dog needs the tiger. If something visits the tiger then the tiger needs the dog. If something is round then it likes the tiger.
The dog visits the tiger.
("dog" "visits" "tiger" "+")
The tiger visits the dog.
("tiger" "visits" "dog" "+")
If something needs the dog then it is round.
((("something" "needs" "dog" "+")) -> ("something" "is" "round" "+"))
If something is blue and it needs the tiger then it is round.
((("something" "is" "blue" "+") ("something" "needs" "tiger" "+")) -> ("something" "is" "round" "+"))
If something likes the tiger then it visits the tiger.
((("something" "likes" "tiger" "+")) -> ("something" "visits" "tiger" "+"))
If the dog likes the tiger and the tiger needs the dog then the dog needs the tiger.
((("dog" "likes" "tiger" "+") ("tiger" "needs" "dog" "+")) -> ("dog" "needs" "tiger" "+"))
If something visits the tiger then the tiger needs the dog.
((("something" "visits" "tiger" "+")) -> ("tiger" "needs" "dog" "+"))
If something is round then it likes the tiger.
((("something" "is" "round" "+")) -> ("something" "likes" "tiger" "+"))
The tiger visits the dog.
True
1
proof
[(triple2)]
("tiger" "visits" "dog" "+")
triple2
The tiger does not visit the dog.
False
1
inv-proof
[(triple2)]
("tiger" "visits" "dog" "-")
triple2
The tiger needs the dog.
True
2
proof
[(((triple1) -> rule5))]
("tiger" "needs" "dog" "+")
((triple1) -> (rule5 % int1))
The tiger needs the dog.
("tiger" "needs" "dog" "+")
int1
The tiger does not need the dog.
False
2
inv-proof
[(((triple1) -> rule5))]
("tiger" "needs" "dog" "-")
((triple1) -> (rule5 % int1))
The tiger needs the dog.
("tiger" "needs" "dog" "+")
int1
The tiger is round.
True
3
proof
[(((((triple1) -> rule5)) -> rule1))]
("tiger" "is" "round" "+")
((((triple1) -> (rule5 % int2))) -> (rule1 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The tiger needs the dog.
("tiger" "needs" "dog" "+")
int2
The tiger is not round.
False
3
inv-proof
[(((((triple1) -> rule5)) -> rule1))]
("tiger" "is" "round" "-")
((((triple1) -> (rule5 % int2))) -> (rule1 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The tiger needs the dog.
("tiger" "needs" "dog" "+")
int2
The tiger likes the tiger.
True
4
proof
[(((((((triple1) -> rule5)) -> rule1)) -> rule6))]
("tiger" "likes" "tiger" "+")
((((((triple1) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The tiger is round.
("tiger" "is" "round" "+")
int2
The tiger needs the dog.
("tiger" "needs" "dog" "+")
int3
The tiger does not like the tiger.
False
4
inv-proof
[(((((((triple1) -> rule5)) -> rule1)) -> rule6))]
("tiger" "likes" "tiger" "-")
((((((triple1) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The tiger is round.
("tiger" "is" "round" "+")
int2
The tiger needs the dog.
("tiger" "needs" "dog" "+")
int3
The dog does not need the tiger.
Unknown
inv-rconc
[@3: The dog needs the tiger.[CWA. Example of deepest failure = (rule4 <- rule6 <- rule1 <- FAIL)]]
("dog" "needs" "tiger" "-")
The dog is round.
Unknown
rconc
[@1: The dog is round.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "is" "round" "+")
The dog does not like the tiger.
Unknown
inv-rconc
[@2: The dog likes the tiger.[CWA. Example of deepest failure = (rule6 <- rule1 <- FAIL)]]
("dog" "likes" "tiger" "-")
The dog is green.
Unknown
random
[@0: The dog is green.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "green" "+")
The dog is not nice.
Unknown
inv-random
[@0: The dog is nice.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "nice" "-")
The dog likes the dog.
Unknown
random
[@0: The dog likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "dog" "+")
The dog is not rough.
Unknown
inv-random
[@0: The dog is rough.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "rough" "-")
The dog needs the dog.
Unknown
random
[@0: The dog needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "dog" "+")
@0: The dog visits the tiger.[(triple1)] The tiger visits the dog.[(triple2)] @1: The tiger needs the dog.[(((triple1) -> rule5))] @2: The tiger is round.[(((((triple1) -> rule5)) -> rule1))] @3: The tiger likes the tiger.[(((((((triple1) -> rule5)) -> rule1)) -> rule6))] @4: The tiger visits the tiger.[(((((((((triple1) -> rule5)) -> rule1)) -> rule6)) -> rule3))]
The dog visits the tiger.
("dog" "visits" "tiger" "+")
triple1
The tiger visits the dog.
("tiger" "visits" "dog" "+")
triple2
The tiger needs the dog.
("tiger" "needs" "dog" "+")
((triple1) -> (rule5 % int1))
The tiger needs the dog.
("tiger" "needs" "dog" "+")
int1
The tiger is round.
("tiger" "is" "round" "+")
((((triple1) -> (rule5 % int2))) -> (rule1 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The tiger needs the dog.
("tiger" "needs" "dog" "+")
int2
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
((((((triple1) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The tiger is round.
("tiger" "is" "round" "+")
int2
The tiger needs the dog.
("tiger" "needs" "dog" "+")
int3
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
((((((((triple1) -> (rule5 % int4))) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int2
The tiger is round.
("tiger" "is" "round" "+")
int3
The tiger needs the dog.
("tiger" "needs" "dog" "+")
int4