The dog chases the lion. The dog is kind. The dog is red. The dog is young. The dog sees the lion. The dog visits the lion. The lion chases the dog. The lion is big. The lion is red. The lion is young. The lion sees the dog. The lion visits the dog. If something sees the lion and it visits the lion then the lion is young. If something sees the dog then it sees the lion. If something sees the dog and it sees the lion then it visits the lion.
The dog chases the lion.
("dog" "chases" "lion" "+")
The dog is kind.
("dog" "is" "kind" "+")
The dog is red.
("dog" "is" "red" "+")
The dog is young.
("dog" "is" "young" "+")
The dog sees the lion.
("dog" "sees" "lion" "+")
The dog visits the lion.
("dog" "visits" "lion" "+")
The lion chases the dog.
("lion" "chases" "dog" "+")
The lion is big.
("lion" "is" "big" "+")
The lion is red.
("lion" "is" "red" "+")
The lion is young.
("lion" "is" "young" "+")
The lion sees the dog.
("lion" "sees" "dog" "+")
The lion visits the dog.
("lion" "visits" "dog" "+")
If something sees the lion and it visits the lion then the lion is young.
((("something" "sees" "lion" "+") ("something" "visits" "lion" "+")) -> ("lion" "is" "young" "+"))
If something sees the dog then it sees the lion.
((("something" "sees" "dog" "+")) -> ("something" "sees" "lion" "+"))
If something sees the dog and it sees the lion then it visits the lion.
((("something" "sees" "dog" "+") ("something" "sees" "lion" "+")) -> ("something" "visits" "lion" "+"))
The dog sees the lion.
True
1
proof
[(triple5)]
("dog" "sees" "lion" "+")
triple5
The lion does not chase the dog.
False
1
inv-proof
[(triple7)]
("lion" "chases" "dog" "-")
triple7
The lion sees the lion.
True
2
proof
[(((triple11) -> rule2))]
("lion" "sees" "lion" "+")
((triple11) -> (rule2 % int1))
The lion sees the lion.
("lion" "sees" "lion" "+")
int1
The lion does not see the lion.
False
2
inv-proof
[(((triple11) -> rule2))]
("lion" "sees" "lion" "-")
((triple11) -> (rule2 % int1))
The lion sees the lion.
("lion" "sees" "lion" "+")
int1
The lion visits the lion.
True
4
proof
[(((triple11 ((triple11) -> rule2)) -> rule3))]
("lion" "visits" "lion" "+")
((triple11 ((triple11) -> (rule2 % int2))) -> (rule3 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
The lion sees the lion.
("lion" "sees" "lion" "+")
int2
The lion does not visit the lion.
False
4
inv-proof
[(((triple11 ((triple11) -> rule2)) -> rule3))]
("lion" "visits" "lion" "-")
((triple11 ((triple11) -> (rule2 % int2))) -> (rule3 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
The lion sees the lion.
("lion" "sees" "lion" "+")
int2
The lion is not nice.
Unknown
inv-random
[@0: The lion is nice.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "nice" "-")
The lion is kind.
Unknown
random
[@0: The lion is kind.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "kind" "+")
The dog does not chase the dog.
Unknown
inv-random
[@0: The dog chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "dog" "-")
The lion chases the lion.
Unknown
random
[@0: The lion chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "lion" "+")
The dog does not visit the dog.
Unknown
inv-random
[@0: The dog visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "dog" "-")
The dog is nice.
Unknown
random
[@0: The dog is nice.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "nice" "+")
@0: The dog chases the lion.[(triple1)] The dog is kind.[(triple2)] The dog is red.[(triple3)] The dog is young.[(triple4)] The dog sees the lion.[(triple5)] The dog visits the lion.[(triple6)] The lion chases the dog.[(triple7)] The lion is big.[(triple8)] The lion is red.[(triple9)] The lion is young.[(triple10 OR ((triple5 triple6) -> rule1) OR ((((triple11) -> rule2) ((triple11 ((triple11) -> rule2)) -> rule3)) -> rule1))] The lion sees the dog.[(triple11)] The lion visits the dog.[(triple12)] @1: The lion sees the lion.[(((triple11) -> rule2))] @2: The lion visits the lion.[(((triple11 ((triple11) -> rule2)) -> rule3))]
The dog chases the lion.
("dog" "chases" "lion" "+")
triple1
The dog is kind.
("dog" "is" "kind" "+")
triple2
The dog is red.
("dog" "is" "red" "+")
triple3
The dog is young.
("dog" "is" "young" "+")
triple4
The dog sees the lion.
("dog" "sees" "lion" "+")
triple5
The dog visits the lion.
("dog" "visits" "lion" "+")
triple6
The lion chases the dog.
("lion" "chases" "dog" "+")
triple7
The lion is big.
("lion" "is" "big" "+")
triple8
The lion is red.
("lion" "is" "red" "+")
triple9
The lion is young.
("lion" "is" "young" "+")
triple10
((triple5 triple6) -> (rule1 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
((((triple11) -> (rule2 % int3)) ((triple11 ((triple11) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion visits the lion.
("lion" "visits" "lion" "+")
int2
The lion sees the lion.
("lion" "sees" "lion" "+")
int3
The lion sees the dog.
("lion" "sees" "dog" "+")
triple11
The lion visits the dog.
("lion" "visits" "dog" "+")
triple12
The lion sees the lion.
("lion" "sees" "lion" "+")
((triple11) -> (rule2 % int1))
The lion sees the lion.
("lion" "sees" "lion" "+")
int1
The lion visits the lion.
("lion" "visits" "lion" "+")
((triple11 ((triple11) -> (rule2 % int2))) -> (rule3 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
The lion sees the lion.
("lion" "sees" "lion" "+")
int2