The dog is not big. The dog is not blue. The dog is not cold. The dog is green. The dog is rough. The dog needs the tiger. The dog sees the tiger. The dog visits the tiger. The tiger is big. The tiger is blue. The tiger is cold. The tiger is not green. The tiger is rough. The tiger needs the dog. The tiger sees the dog. The tiger visits the dog. If something visits the tiger then it sees the tiger. If something is cold and it needs the dog then it sees the tiger.
The dog is not big.
("dog" "is" "big" "-")
The dog is not blue.
("dog" "is" "blue" "-")
The dog is not cold.
("dog" "is" "cold" "-")
The dog is green.
("dog" "is" "green" "+")
The dog is rough.
("dog" "is" "rough" "+")
The dog needs the tiger.
("dog" "needs" "tiger" "+")
The dog sees the tiger.
("dog" "sees" "tiger" "+")
The dog visits the tiger.
("dog" "visits" "tiger" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger is not green.
("tiger" "is" "green" "-")
The tiger is rough.
("tiger" "is" "rough" "+")
The tiger needs the dog.
("tiger" "needs" "dog" "+")
The tiger sees the dog.
("tiger" "sees" "dog" "+")
The tiger visits the dog.
("tiger" "visits" "dog" "+")
If something visits the tiger then it sees the tiger.
((("something" "visits" "tiger" "+")) -> ("something" "sees" "tiger" "+"))
If something is cold and it needs the dog then it sees the tiger.
((("something" "is" "cold" "+") ("something" "needs" "dog" "+")) -> ("something" "sees" "tiger" "+"))
The tiger is cold.
True
1
proof
[(triple11)]
("tiger" "is" "cold" "+")
triple11
The dog is not rough.
False
1
inv-proof
[(triple5)]
("dog" "is" "rough" "-")
triple5
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 visits the dog.
Unknown
random
[@0: The dog visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "dog" "+")
@0: The dog is green.[(triple4)] The dog is not big.[(triple1)] The dog is not blue.[(triple2)] The dog is not cold.[(triple3)] The dog is rough.[(triple5)] The dog needs the tiger.[(triple6)] The dog sees the tiger.[(triple7 OR ((triple8) -> rule1))] The dog visits the tiger.[(triple8)] The tiger is big.[(triple9)] The tiger is blue.[(triple10)] The tiger is cold.[(triple11)] The tiger is not green.[(triple12)] The tiger is rough.[(triple13)] The tiger needs the dog.[(triple14)] The tiger sees the dog.[(triple15)] The tiger visits the dog.[(triple16)] @1: The tiger sees the tiger.[(((triple11 triple14) -> rule2))]
The dog is green.
("dog" "is" "green" "+")
triple4
The dog is not big.
("dog" "is" "big" "-")
triple1
The dog is not blue.
("dog" "is" "blue" "-")
triple2
The dog is not cold.
("dog" "is" "cold" "-")
triple3
The dog is rough.
("dog" "is" "rough" "+")
triple5
The dog needs the tiger.
("dog" "needs" "tiger" "+")
triple6
The dog sees the tiger.
("dog" "sees" "tiger" "+")
triple7
((triple8) -> (rule1 % int1))
The dog sees the tiger.
("dog" "sees" "tiger" "+")
int1
The dog visits the tiger.
("dog" "visits" "tiger" "+")
triple8
The tiger is big.
("tiger" "is" "big" "+")
triple9
The tiger is blue.
("tiger" "is" "blue" "+")
triple10
The tiger is cold.
("tiger" "is" "cold" "+")
triple11
The tiger is not green.
("tiger" "is" "green" "-")
triple12
The tiger is rough.
("tiger" "is" "rough" "+")
triple13
The tiger needs the dog.
("tiger" "needs" "dog" "+")
triple14
The tiger sees the dog.
("tiger" "sees" "dog" "+")
triple15
The tiger visits the dog.
("tiger" "visits" "dog" "+")
triple16
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
((triple11 triple14) -> (rule2 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1