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