The dog is red. The dog is young. The dog visits the tiger. The tiger is nice. The tiger needs the dog. The tiger sees the dog. The tiger visits the dog. If someone is nice and green then they see the tiger. If someone is red then they are nice.
The dog is red.
("dog" "is" "red" "+")
The dog is young.
("dog" "is" "young" "+")
The dog visits the tiger.
("dog" "visits" "tiger" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
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 is nice and green then they see the tiger.
((("someone" "is" "nice" "+") ("someone" "is" "green" "+")) -> ("someone" "sees" "tiger" "+"))
If someone is red then they are nice.
((("someone" "is" "red" "+")) -> ("someone" "is" "nice" "+"))
The dog is young.
True
1
proof
[(triple2)]
("dog" "is" "young" "+")
triple2
The dog is not red.
False
1
inv-proof
[(triple1)]
("dog" "is" "red" "-")
triple1
The dog is nice.
True
2
proof
[(((triple1) -> rule2))]
("dog" "is" "nice" "+")
((triple1) -> (rule2 % int1))
The dog is nice.
("dog" "is" "nice" "+")
int1
The dog is not nice.
False
2
inv-proof
[(((triple1) -> rule2))]
("dog" "is" "nice" "-")
((triple1) -> (rule2 % int1))
The dog is nice.
("dog" "is" "nice" "+")
int1
The tiger does not see the tiger.
Unknown
inv-rconc
[@1: The tiger sees the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "sees" "tiger" "-")
The dog sees the tiger.
Unknown
rconc
[@1: The dog sees the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "sees" "tiger" "+")
The dog does not need the dog.
Unknown
inv-random
[@0: The dog needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "dog" "-")
The dog is round.
Unknown
random
[@0: The dog is round.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "round" "+")
@0: The dog is red.[(triple1)] The dog is young.[(triple2)] The dog visits the tiger.[(triple3)] The tiger is nice.[(triple4)] The tiger needs the dog.[(triple5)] The tiger sees the dog.[(triple6)] The tiger visits the dog.[(triple7)] @1: The dog is nice.[(((triple1) -> rule2))]
The dog is red.
("dog" "is" "red" "+")
triple1
The dog is young.
("dog" "is" "young" "+")
triple2
The dog visits the tiger.
("dog" "visits" "tiger" "+")
triple3
The tiger is nice.
("tiger" "is" "nice" "+")
triple4
The tiger needs the dog.
("tiger" "needs" "dog" "+")
triple5
The tiger sees the dog.
("tiger" "sees" "dog" "+")
triple6
The tiger visits the dog.
("tiger" "visits" "dog" "+")
triple7
The dog is nice.
("dog" "is" "nice" "+")
((triple1) -> (rule2 % int1))
The dog is nice.
("dog" "is" "nice" "+")
int1