The dog chases the tiger. The dog is big. The dog is blue. The dog is cold. The dog is kind. The dog is red. The dog needs the tiger. The dog sees the tiger. The tiger chases the dog. The tiger is big. The tiger is blue. The tiger is cold. The tiger is kind. The tiger is red. The tiger needs the dog. The tiger sees the dog. If someone chases the tiger then they need the dog. If someone sees the dog then the dog chases the tiger. If someone needs the tiger and they are kind then they chase the tiger. If someone needs the tiger and they see the tiger then they need the dog. If someone is blue then they chase the tiger. If someone sees the dog then they chase the dog. If someone needs the tiger and they see the tiger then the tiger needs the dog. If someone needs the tiger and they need the dog then the tiger chases the dog.
The dog chases the tiger.
("dog" "chases" "tiger" "+")
The dog is big.
("dog" "is" "big" "+")
The dog is blue.
("dog" "is" "blue" "+")
The dog is cold.
("dog" "is" "cold" "+")
The dog is kind.
("dog" "is" "kind" "+")
The dog is red.
("dog" "is" "red" "+")
The dog needs the tiger.
("dog" "needs" "tiger" "+")
The dog sees the tiger.
("dog" "sees" "tiger" "+")
The tiger chases the dog.
("tiger" "chases" "dog" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger is red.
("tiger" "is" "red" "+")
The tiger needs the dog.
("tiger" "needs" "dog" "+")
The tiger sees the dog.
("tiger" "sees" "dog" "+")
If someone chases the tiger then they need the dog.
((("someone" "chases" "tiger" "+")) -> ("someone" "needs" "dog" "+"))
If someone sees the dog then the dog chases the tiger.
((("someone" "sees" "dog" "+")) -> ("dog" "chases" "tiger" "+"))
If someone needs the tiger and they are kind then they chase the tiger.
((("someone" "needs" "tiger" "+") ("someone" "is" "kind" "+")) -> ("someone" "chases" "tiger" "+"))
If someone needs the tiger and they see the tiger then they need the dog.
((("someone" "needs" "tiger" "+") ("someone" "sees" "tiger" "+")) -> ("someone" "needs" "dog" "+"))
If someone is blue then they chase the tiger.
((("someone" "is" "blue" "+")) -> ("someone" "chases" "tiger" "+"))
If someone sees the dog then they chase the dog.
((("someone" "sees" "dog" "+")) -> ("someone" "chases" "dog" "+"))
If someone needs the tiger and they see the tiger then the tiger needs the dog.
((("someone" "needs" "tiger" "+") ("someone" "sees" "tiger" "+")) -> ("tiger" "needs" "dog" "+"))
If someone needs the tiger and they need the dog then the tiger chases the dog.
((("someone" "needs" "tiger" "+") ("someone" "needs" "dog" "+")) -> ("tiger" "chases" "dog" "+"))
The tiger is blue.
True
1
proof
[(triple11)]
("tiger" "is" "blue" "+")
triple11
The tiger does not need the dog.
False
1
inv-proof
[(triple15 OR ((triple7 triple8) -> rule7) OR ((((triple11) -> rule5)) -> rule1))]
("tiger" "needs" "dog" "-")
triple15
((triple7 triple8) -> (rule7 % int1))
The tiger needs the dog.
("tiger" "needs" "dog" "+")
int1
((((triple11) -> (rule5 % int2))) -> (rule1 % int1))
The tiger needs the dog.
("tiger" "needs" "dog" "+")
int1
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int2
The tiger chases the tiger.
True
2
proof
[(((triple11) -> rule5))]
("tiger" "chases" "tiger" "+")
((triple11) -> (rule5 % int1))
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int1
The tiger does not chase the tiger.
False
2
inv-proof
[(((triple11) -> rule5))]
("tiger" "chases" "tiger" "-")
((triple11) -> (rule5 % int1))
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int1
The dog does not chase the dog.
Unknown
inv-rconc
[@1: The dog chases the dog.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("dog" "chases" "dog" "-")
The dog sees the dog.
Unknown
random
[@0: The dog sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "dog" "+")
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 tiger sees the tiger.
Unknown
random
[@0: The tiger sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "tiger" "+")
@0: The dog chases the tiger.[(triple1 OR ((triple16) -> rule2) OR ((triple3) -> rule5) OR ((triple7 triple5) -> rule3))] The dog is big.[(triple2)] The dog is blue.[(triple3)] The dog is cold.[(triple4)] The dog is kind.[(triple5)] The dog is red.[(triple6)] The dog needs the tiger.[(triple7)] The dog sees the tiger.[(triple8)] The tiger chases the dog.[(triple9 OR ((triple16) -> rule6) OR ((triple7 ((triple1) -> rule1)) -> rule8) OR ((triple7 ((triple7 triple8) -> rule4)) -> rule8) OR ((triple7 ((((triple16) -> rule2)) -> rule1)) -> rule8) OR ((triple7 ((((triple3) -> rule5)) -> rule1)) -> rule8) OR ((triple7 ((((triple7 triple5) -> rule3)) -> rule1)) -> rule8))] The tiger is big.[(triple10)] The tiger is blue.[(triple11)] The tiger is cold.[(triple12)] The tiger is kind.[(triple13)] The tiger is red.[(triple14)] The tiger needs the dog.[(triple15 OR ((triple7 triple8) -> rule7) OR ((((triple11) -> rule5)) -> rule1))] The tiger sees the dog.[(triple16)] @1: The dog needs the dog.[(((triple1) -> rule1) OR ((triple7 triple8) -> rule4) OR ((((triple16) -> rule2)) -> rule1) OR ((((triple3) -> rule5)) -> rule1) OR ((((triple7 triple5) -> rule3)) -> rule1))] The tiger chases the tiger.[(((triple11) -> rule5))]
The dog chases the tiger.
("dog" "chases" "tiger" "+")
triple1
((triple16) -> (rule2 % int1))
The dog chases the tiger.
("dog" "chases" "tiger" "+")
int1
((triple3) -> (rule5 % int1))
The dog chases the tiger.
("dog" "chases" "tiger" "+")
int1
((triple7 triple5) -> (rule3 % int1))
The dog chases the tiger.
("dog" "chases" "tiger" "+")
int1
The dog is big.
("dog" "is" "big" "+")
triple2
The dog is blue.
("dog" "is" "blue" "+")
triple3
The dog is cold.
("dog" "is" "cold" "+")
triple4
The dog is kind.
("dog" "is" "kind" "+")
triple5
The dog is red.
("dog" "is" "red" "+")
triple6
The dog needs the tiger.
("dog" "needs" "tiger" "+")
triple7
The dog sees the tiger.
("dog" "sees" "tiger" "+")
triple8
The tiger chases the dog.
("tiger" "chases" "dog" "+")
triple9
((triple16) -> (rule6 % int1))
The tiger chases the dog.
("tiger" "chases" "dog" "+")
int1
((triple7 ((triple1) -> (rule1 % int2))) -> (rule8 % int1))
The tiger chases the dog.
("tiger" "chases" "dog" "+")
int1
The dog needs the dog.
("dog" "needs" "dog" "+")
int2
((triple7 ((triple7 triple8) -> (rule4 % int2))) -> (rule8 % int1))
The tiger chases the dog.
("tiger" "chases" "dog" "+")
int1
The dog needs the dog.
("dog" "needs" "dog" "+")
int2
((triple7 ((((triple16) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
The tiger chases the dog.
("tiger" "chases" "dog" "+")
int1
The dog needs the dog.
("dog" "needs" "dog" "+")
int2
The dog chases the tiger.
("dog" "chases" "tiger" "+")
int3
((triple7 ((((triple3) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
The tiger chases the dog.
("tiger" "chases" "dog" "+")
int1
The dog needs the dog.
("dog" "needs" "dog" "+")
int2
The dog chases the tiger.
("dog" "chases" "tiger" "+")
int3
((triple7 ((((triple7 triple5) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
The tiger chases the dog.
("tiger" "chases" "dog" "+")
int1
The dog needs the dog.
("dog" "needs" "dog" "+")
int2
The dog chases the tiger.
("dog" "chases" "tiger" "+")
int3
The tiger is big.
("tiger" "is" "big" "+")
triple10
The tiger is blue.
("tiger" "is" "blue" "+")
triple11
The tiger is cold.
("tiger" "is" "cold" "+")
triple12
The tiger is kind.
("tiger" "is" "kind" "+")
triple13
The tiger is red.
("tiger" "is" "red" "+")
triple14
The tiger needs the dog.
("tiger" "needs" "dog" "+")
triple15
((triple7 triple8) -> (rule7 % int1))
The tiger needs the dog.
("tiger" "needs" "dog" "+")
int1
((((triple11) -> (rule5 % int2))) -> (rule1 % int1))
The tiger needs the dog.
("tiger" "needs" "dog" "+")
int1
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int2
The tiger sees the dog.
("tiger" "sees" "dog" "+")
triple16
The dog needs the dog.
("dog" "needs" "dog" "+")
((triple1) -> (rule1 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
((triple7 triple8) -> (rule4 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
((((triple16) -> (rule2 % int2))) -> (rule1 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The dog chases the tiger.
("dog" "chases" "tiger" "+")
int2
((((triple3) -> (rule5 % int2))) -> (rule1 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The dog chases the tiger.
("dog" "chases" "tiger" "+")
int2
((((triple7 triple5) -> (rule3 % int2))) -> (rule1 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The dog chases the tiger.
("dog" "chases" "tiger" "+")
int2
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
((triple11) -> (rule5 % int1))
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int1