The cat eats the dog. The dog eats the cat. The dog eats the lion. The dog is big. The dog is kind. The dog is rough. The dog needs the cat. The dog needs the lion. The dog sees the cat. The dog sees the lion. The lion eats the cat. The lion is kind. The lion is round. The lion needs the cat. The lion sees the dog. If something sees the dog and the dog is blue then it sees the lion. If something sees the lion then it is blue. If something sees the dog then the dog eats the lion.
The cat eats the dog.
("cat" "eats" "dog" "+")
The dog eats the cat.
("dog" "eats" "cat" "+")
The dog eats the lion.
("dog" "eats" "lion" "+")
The dog is big.
("dog" "is" "big" "+")
The dog is kind.
("dog" "is" "kind" "+")
The dog is rough.
("dog" "is" "rough" "+")
The dog needs the cat.
("dog" "needs" "cat" "+")
The dog needs the lion.
("dog" "needs" "lion" "+")
The dog sees the cat.
("dog" "sees" "cat" "+")
The dog sees the lion.
("dog" "sees" "lion" "+")
The lion eats the cat.
("lion" "eats" "cat" "+")
The lion is kind.
("lion" "is" "kind" "+")
The lion is round.
("lion" "is" "round" "+")
The lion needs the cat.
("lion" "needs" "cat" "+")
The lion sees the dog.
("lion" "sees" "dog" "+")
If something sees the dog and the dog is blue then it sees the lion.
((("something" "sees" "dog" "+") ("dog" "is" "blue" "+")) -> ("something" "sees" "lion" "+"))
If something sees the lion then it is blue.
((("something" "sees" "lion" "+")) -> ("something" "is" "blue" "+"))
If something sees the dog then the dog eats the lion.
((("something" "sees" "dog" "+")) -> ("dog" "eats" "lion" "+"))
The dog needs the cat.
True
1
proof
[(triple7)]
("dog" "needs" "cat" "+")
triple7
The dog does not need the lion.
False
1
inv-proof
[(triple8)]
("dog" "needs" "lion" "-")
triple8
The dog is blue.
True
2
proof
[(((triple10) -> rule2))]
("dog" "is" "blue" "+")
((triple10) -> (rule2 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
The dog is not blue.
False
2
inv-proof
[(((triple10) -> rule2))]
("dog" "is" "blue" "-")
((triple10) -> (rule2 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
The lion sees the lion.
True
4
proof
[(((triple15 ((triple10) -> rule2)) -> rule1))]
("lion" "sees" "lion" "+")
((triple15 ((triple10) -> (rule2 % int2))) -> (rule1 % int1))
The lion sees the lion.
("lion" "sees" "lion" "+")
int1
The dog is blue.
("dog" "is" "blue" "+")
int2
The lion does not see the lion.
False
4
inv-proof
[(((triple15 ((triple10) -> rule2)) -> rule1))]
("lion" "sees" "lion" "-")
((triple15 ((triple10) -> (rule2 % int2))) -> (rule1 % int1))
The lion sees the lion.
("lion" "sees" "lion" "+")
int1
The dog is blue.
("dog" "is" "blue" "+")
int2
The lion is blue.
True
5
proof
[(((((triple15 ((triple10) -> rule2)) -> rule1)) -> rule2))]
("lion" "is" "blue" "+")
((((triple15 ((triple10) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The lion sees the lion.
("lion" "sees" "lion" "+")
int2
The dog is blue.
("dog" "is" "blue" "+")
int3
The lion is not blue.
False
5
inv-proof
[(((((triple15 ((triple10) -> rule2)) -> rule1)) -> rule2))]
("lion" "is" "blue" "-")
((((triple15 ((triple10) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The lion sees the lion.
("lion" "sees" "lion" "+")
int2
The dog is blue.
("dog" "is" "blue" "+")
int3
The cat does not see the lion.
Unknown
inv-rconc
[@1: The cat sees the lion.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "sees" "lion" "-")
The cat is blue.
Unknown
rconc
[@2: The cat is blue.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("cat" "is" "blue" "+")
The cat does not need the dog.
Unknown
inv-random
[@0: The cat needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "dog" "-")
The lion needs the lion.
Unknown
random
[@0: The lion needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "lion" "+")
The cat is not kind.
Unknown
inv-random
[@0: The cat is kind.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "kind" "-")
The cat is round.
Unknown
random
[@0: The cat is round.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "round" "+")
The cat does not eat the lion.
Unknown
inv-random
[@0: The cat eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "lion" "-")
The cat sees the dog.
Unknown
random
[@0: The cat sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "dog" "+")
@0: The cat eats the dog.[(triple1)] The dog eats the cat.[(triple2)] The dog eats the lion.[(triple3 OR ((triple15) -> rule3))] The dog is big.[(triple4)] The dog is kind.[(triple5)] The dog is rough.[(triple6)] The dog needs the cat.[(triple7)] The dog needs the lion.[(triple8)] The dog sees the cat.[(triple9)] The dog sees the lion.[(triple10)] The lion eats the cat.[(triple11)] The lion is kind.[(triple12)] The lion is round.[(triple13)] The lion needs the cat.[(triple14)] The lion sees the dog.[(triple15)] @1: The dog is blue.[(((triple10) -> rule2))] @2: The lion sees the lion.[(((triple15 ((triple10) -> rule2)) -> rule1))] @3: The lion is blue.[(((((triple15 ((triple10) -> rule2)) -> rule1)) -> rule2))]
The cat eats the dog.
("cat" "eats" "dog" "+")
triple1
The dog eats the cat.
("dog" "eats" "cat" "+")
triple2
The dog eats the lion.
("dog" "eats" "lion" "+")
triple3
((triple15) -> (rule3 % int1))
The dog eats the lion.
("dog" "eats" "lion" "+")
int1
The dog is big.
("dog" "is" "big" "+")
triple4
The dog is kind.
("dog" "is" "kind" "+")
triple5
The dog is rough.
("dog" "is" "rough" "+")
triple6
The dog needs the cat.
("dog" "needs" "cat" "+")
triple7
The dog needs the lion.
("dog" "needs" "lion" "+")
triple8
The dog sees the cat.
("dog" "sees" "cat" "+")
triple9
The dog sees the lion.
("dog" "sees" "lion" "+")
triple10
The lion eats the cat.
("lion" "eats" "cat" "+")
triple11
The lion is kind.
("lion" "is" "kind" "+")
triple12
The lion is round.
("lion" "is" "round" "+")
triple13
The lion needs the cat.
("lion" "needs" "cat" "+")
triple14
The lion sees the dog.
("lion" "sees" "dog" "+")
triple15
The dog is blue.
("dog" "is" "blue" "+")
((triple10) -> (rule2 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
The lion sees the lion.
("lion" "sees" "lion" "+")
((triple15 ((triple10) -> (rule2 % int2))) -> (rule1 % int1))
The lion sees the lion.
("lion" "sees" "lion" "+")
int1
The dog is blue.
("dog" "is" "blue" "+")
int2
The lion is blue.
("lion" "is" "blue" "+")
((((triple15 ((triple10) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The lion sees the lion.
("lion" "sees" "lion" "+")
int2
The dog is blue.
("dog" "is" "blue" "+")
int3