The dog is green. The dog likes the tiger. The dog needs the tiger. The dog visits the tiger. The tiger is not blue. The tiger is green. The tiger is kind. The tiger is nice. The tiger is red. The tiger likes the dog. The tiger needs the dog. The tiger visits the dog. If the tiger visits the dog then the dog needs the tiger. If something is blue and it does not need the dog then it visits the tiger. If something likes the tiger then it does not visit the dog.
The dog is green.
("dog" "is" "green" "+")
The dog likes the tiger.
("dog" "likes" "tiger" "+")
The dog needs the tiger.
("dog" "needs" "tiger" "+")
The dog visits the tiger.
("dog" "visits" "tiger" "+")
The tiger is not blue.
("tiger" "is" "blue" "-")
The tiger is green.
("tiger" "is" "green" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger is red.
("tiger" "is" "red" "+")
The tiger likes the dog.
("tiger" "likes" "dog" "+")
The tiger needs the dog.
("tiger" "needs" "dog" "+")
The tiger visits the dog.
("tiger" "visits" "dog" "+")
If the tiger visits the dog then the dog needs the tiger.
((("tiger" "visits" "dog" "+")) -> ("dog" "needs" "tiger" "+"))
If something is blue and it does not need the dog then it visits the tiger.
((("something" "is" "blue" "+") ("something" "needs" "dog" "~")) -> ("something" "visits" "tiger" "+"))
If something likes the tiger then it does not visit the dog.
((("something" "likes" "tiger" "+")) -> ("something" "visits" "dog" "-"))
The tiger is not blue.
True
1
proof
[(triple5)]
("tiger" "is" "blue" "-")
triple5
The tiger does not need the dog.
False
1
inv-proof
[(triple11)]
("tiger" "needs" "dog" "-")
triple11
The dog does not visit the dog.
True
2
proof
[(((triple2) -> rule3))]
("dog" "visits" "dog" "-")
((triple2) -> (rule3 % int1))
The dog does not visit the dog.
("dog" "visits" "dog" "-")
int1
The dog visits the dog.
False
2
inv-proof
[(((triple2) -> rule3))]
("dog" "visits" "dog" "+")
((triple2) -> (rule3 % int1))
The dog does not visit the dog.
("dog" "visits" "dog" "-")
int1
The tiger does not visit the tiger.
Unknown
inv-rconc
[@1: The tiger visits the tiger.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "visits" "tiger" "-")
The dog is kind.
Unknown
random
[@0: The dog is kind.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "kind" "+")
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 needs the dog.
Unknown
random
[@0: The dog needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "dog" "+")
@0: The dog is green.[(triple1)] The dog likes the tiger.[(triple2)] The dog needs the tiger.[(triple3 OR ((triple12) -> rule1))] The dog visits the tiger.[(triple4)] The tiger is green.[(triple6)] The tiger is kind.[(triple7)] The tiger is nice.[(triple8)] The tiger is not blue.[(triple5)] The tiger is red.[(triple9)] The tiger likes the dog.[(triple10)] The tiger needs the dog.[(triple11)] The tiger visits the dog.[(triple12)] @1: The dog does not visit the dog.[(((triple2) -> rule3))]
The dog is green.
("dog" "is" "green" "+")
triple1
The dog likes the tiger.
("dog" "likes" "tiger" "+")
triple2
The dog needs the tiger.
("dog" "needs" "tiger" "+")
triple3
((triple12) -> (rule1 % int1))
The dog needs the tiger.
("dog" "needs" "tiger" "+")
int1
The dog visits the tiger.
("dog" "visits" "tiger" "+")
triple4
The tiger is green.
("tiger" "is" "green" "+")
triple6
The tiger is kind.
("tiger" "is" "kind" "+")
triple7
The tiger is nice.
("tiger" "is" "nice" "+")
triple8
The tiger is not blue.
("tiger" "is" "blue" "-")
triple5
The tiger is red.
("tiger" "is" "red" "+")
triple9
The tiger likes the dog.
("tiger" "likes" "dog" "+")
triple10
The tiger needs the dog.
("tiger" "needs" "dog" "+")
triple11
The tiger visits the dog.
("tiger" "visits" "dog" "+")
triple12
The dog does not visit the dog.
("dog" "visits" "dog" "-")
((triple2) -> (rule3 % int1))
The dog does not visit the dog.
("dog" "visits" "dog" "-")
int1