The dog sees the lion. The dog sees the squirrel. The dog visits the squirrel. The lion eats the dog. The lion sees the dog. The squirrel eats the dog. The squirrel visits the lion. If something sees the squirrel then it is young.
The dog sees the lion.
("dog" "sees" "lion" "+")
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
The lion eats the dog.
("lion" "eats" "dog" "+")
The lion sees the dog.
("lion" "sees" "dog" "+")
The squirrel eats the dog.
("squirrel" "eats" "dog" "+")
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
If something sees the squirrel then it is young.
((("something" "sees" "squirrel" "+")) -> ("something" "is" "young" "+"))
The dog sees the lion.
True
1
proof
[(triple1)]
("dog" "sees" "lion" "+")
triple1
The lion does not see the dog.
False
1
inv-proof
[(triple5)]
("lion" "sees" "dog" "-")
triple5
The dog is young.
True
2
proof
[(((triple2) -> rule1))]
("dog" "is" "young" "+")
((triple2) -> (rule1 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The dog is not young.
False
2
inv-proof
[(((triple2) -> rule1))]
("dog" "is" "young" "-")
((triple2) -> (rule1 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The lion is not young.
Unknown
inv-rconc
[@1: The lion is young.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "is" "young" "-")
The squirrel is young.
Unknown
rconc
[@1: The squirrel is young.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "is" "young" "+")
The lion does not visit the squirrel.
Unknown
inv-random
[@0: The lion visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "squirrel" "-")
The lion sees the squirrel.
Unknown
random
[@0: The lion sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "squirrel" "+")
@0: The dog sees the lion.[(triple1)] The dog sees the squirrel.[(triple2)] The dog visits the squirrel.[(triple3)] The lion eats the dog.[(triple4)] The lion sees the dog.[(triple5)] The squirrel eats the dog.[(triple6)] The squirrel visits the lion.[(triple7)] @1: The dog is young.[(((triple2) -> rule1))]
The dog sees the lion.
("dog" "sees" "lion" "+")
triple1
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
triple2
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
triple3
The lion eats the dog.
("lion" "eats" "dog" "+")
triple4
The lion sees the dog.
("lion" "sees" "dog" "+")
triple5
The squirrel eats the dog.
("squirrel" "eats" "dog" "+")
triple6
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
triple7
The dog is young.
("dog" "is" "young" "+")
((triple2) -> (rule1 % int1))
The dog is young.
("dog" "is" "young" "+")
int1