The dog is kind. The dog is red. The dog is rough. The dog is young. The dog needs the tiger. The dog sees the tiger. The dog visits the tiger. The tiger is rough. The tiger is young. The tiger needs the dog. The tiger sees the dog. The tiger visits the dog. If someone visits the dog then the dog is blue. Blue, young people are kind. If someone sees the dog then they visit the tiger. If someone visits the dog then the dog sees the tiger. If someone visits the dog and the dog is young then they see the dog. If the tiger is blue then the tiger needs the dog.
The dog is kind.
("dog" "is" "kind" "+")
The dog is red.
("dog" "is" "red" "+")
The dog is rough.
("dog" "is" "rough" "+")
The dog is young.
("dog" "is" "young" "+")
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 rough.
("tiger" "is" "rough" "+")
The tiger is young.
("tiger" "is" "young" "+")
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 someone visits the dog then the dog is blue.
((("someone" "visits" "dog" "+")) -> ("dog" "is" "blue" "+"))
Blue, young people are kind.
((("someone" "is" "blue" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "kind" "+"))
If someone sees the dog then they visit the tiger.
((("someone" "sees" "dog" "+")) -> ("someone" "visits" "tiger" "+"))
If someone visits the dog then the dog sees the tiger.
((("someone" "visits" "dog" "+")) -> ("dog" "sees" "tiger" "+"))
If someone visits the dog and the dog is young then they see the dog.
((("someone" "visits" "dog" "+") ("dog" "is" "young" "+")) -> ("someone" "sees" "dog" "+"))
If the tiger is blue then the tiger needs the dog.
((("tiger" "is" "blue" "+")) -> ("tiger" "needs" "dog" "+"))
The dog visits the tiger.
True
1
proof
[(triple7)]
("dog" "visits" "tiger" "+")
triple7
The tiger does not need the dog.
False
1
inv-proof
[(triple10)]
("tiger" "needs" "dog" "-")
triple10
The tiger is not kind.
Unknown
inv-rconc
[@1: The tiger is kind.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "is" "kind" "-")
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 kind.[(triple1 OR ((((triple12) -> rule1) triple4) -> rule2))] The dog is red.[(triple2)] The dog is rough.[(triple3)] The dog is young.[(triple4)] The dog needs the tiger.[(triple5)] The dog sees the tiger.[(triple6 OR ((triple12) -> rule4))] The dog visits the tiger.[(triple7)] The tiger is rough.[(triple8)] The tiger is young.[(triple9)] The tiger needs the dog.[(triple10)] The tiger sees the dog.[(triple11 OR ((triple12 triple4) -> rule5))] The tiger visits the dog.[(triple12)] @1: The dog is blue.[(((triple12) -> rule1))] The tiger visits the tiger.[(((triple11) -> rule3) OR ((((triple12 triple4) -> rule5)) -> rule3))]
The dog is kind.
("dog" "is" "kind" "+")
triple1
((((triple12) -> (rule1 % int2)) triple4) -> (rule2 % int1))
The dog is kind.
("dog" "is" "kind" "+")
int1
The dog is blue.
("dog" "is" "blue" "+")
int2
The dog is red.
("dog" "is" "red" "+")
triple2
The dog is rough.
("dog" "is" "rough" "+")
triple3
The dog is young.
("dog" "is" "young" "+")
triple4
The dog needs the tiger.
("dog" "needs" "tiger" "+")
triple5
The dog sees the tiger.
("dog" "sees" "tiger" "+")
triple6
((triple12) -> (rule4 % int1))
The dog sees the tiger.
("dog" "sees" "tiger" "+")
int1
The dog visits the tiger.
("dog" "visits" "tiger" "+")
triple7
The tiger is rough.
("tiger" "is" "rough" "+")
triple8
The tiger is young.
("tiger" "is" "young" "+")
triple9
The tiger needs the dog.
("tiger" "needs" "dog" "+")
triple10
The tiger sees the dog.
("tiger" "sees" "dog" "+")
triple11
((triple12 triple4) -> (rule5 % int1))
The tiger sees the dog.
("tiger" "sees" "dog" "+")
int1
The tiger visits the dog.
("tiger" "visits" "dog" "+")
triple12
The dog is blue.
("dog" "is" "blue" "+")
((triple12) -> (rule1 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
((triple11) -> (rule3 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
((((triple12 triple4) -> (rule5 % int2))) -> (rule3 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
The tiger sees the dog.
("tiger" "sees" "dog" "+")
int2