The cow visits the dog. The dog chases the tiger. The lion visits the cow. The tiger visits the dog. If someone is big then they are young. If someone is kind then they chase the cow. If someone chases the dog and the dog sees the cow then the dog visits the cow. If the dog sees the lion then the dog visits the cow. If someone visits the lion and they chase the lion then the lion sees the tiger. If someone is young then they see the cow. If the tiger visits the dog then the dog is big. If someone sees the tiger then they are young.
The cow visits the dog.
("cow" "visits" "dog" "+")
The dog chases the tiger.
("dog" "chases" "tiger" "+")
The lion visits the cow.
("lion" "visits" "cow" "+")
The tiger visits the dog.
("tiger" "visits" "dog" "+")
If someone is big then they are young.
((("someone" "is" "big" "+")) -> ("someone" "is" "young" "+"))
If someone is kind then they chase the cow.
((("someone" "is" "kind" "+")) -> ("someone" "chases" "cow" "+"))
If someone chases the dog and the dog sees the cow then the dog visits the cow.
((("someone" "chases" "dog" "+") ("dog" "sees" "cow" "+")) -> ("dog" "visits" "cow" "+"))
If the dog sees the lion then the dog visits the cow.
((("dog" "sees" "lion" "+")) -> ("dog" "visits" "cow" "+"))
If someone visits the lion and they chase the lion then the lion sees the tiger.
((("someone" "visits" "lion" "+") ("someone" "chases" "lion" "+")) -> ("lion" "sees" "tiger" "+"))
If someone is young then they see the cow.
((("someone" "is" "young" "+")) -> ("someone" "sees" "cow" "+"))
If the tiger visits the dog then the dog is big.
((("tiger" "visits" "dog" "+")) -> ("dog" "is" "big" "+"))
If someone sees the tiger then they are young.
((("someone" "sees" "tiger" "+")) -> ("someone" "is" "young" "+"))
The lion visits the cow.
True
1
proof
[(triple3)]
("lion" "visits" "cow" "+")
triple3
The tiger does not visit the dog.
False
1
inv-proof
[(triple4)]
("tiger" "visits" "dog" "-")
triple4
The dog is big.
True
2
proof
[(((triple4) -> rule7))]
("dog" "is" "big" "+")
((triple4) -> (rule7 % int1))
The dog is big.
("dog" "is" "big" "+")
int1
The dog is not big.
False
2
inv-proof
[(((triple4) -> rule7))]
("dog" "is" "big" "-")
((triple4) -> (rule7 % int1))
The dog is big.
("dog" "is" "big" "+")
int1
The dog is young.
True
3
proof
[(((((triple4) -> rule7)) -> rule1))]
("dog" "is" "young" "+")
((((triple4) -> (rule7 % int2))) -> (rule1 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The dog is big.
("dog" "is" "big" "+")
int2
The dog is not young.
False
3
inv-proof
[(((((triple4) -> rule7)) -> rule1))]
("dog" "is" "young" "-")
((((triple4) -> (rule7 % int2))) -> (rule1 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The dog is big.
("dog" "is" "big" "+")
int2
The dog sees the cow.
True
4
proof
[(((((((triple4) -> rule7)) -> rule1)) -> rule6))]
("dog" "sees" "cow" "+")
((((((triple4) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The dog sees the cow.
("dog" "sees" "cow" "+")
int1
The dog is young.
("dog" "is" "young" "+")
int2
The dog is big.
("dog" "is" "big" "+")
int3
The dog does not see the cow.
False
4
inv-proof
[(((((((triple4) -> rule7)) -> rule1)) -> rule6))]
("dog" "sees" "cow" "-")
((((((triple4) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The dog sees the cow.
("dog" "sees" "cow" "+")
int1
The dog is young.
("dog" "is" "young" "+")
int2
The dog is big.
("dog" "is" "big" "+")
int3
The lion does not see the tiger.
Unknown
inv-rconc
[@1: The lion sees the tiger.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("lion" "sees" "tiger" "-")
The dog chases the cow.
Unknown
rconc
[@1: The dog chases the cow.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "chases" "cow" "+")
The lion does not see the cow.
Unknown
inv-rconc
[@3: The lion sees the cow.[CWA. Example of deepest failure = (rule6 <- rule8 <- rule5 <- FAIL)]]
("lion" "sees" "cow" "-")
The cow chases the cow.
Unknown
rconc
[@1: The cow chases the cow.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "chases" "cow" "+")
The dog is not blue.
Unknown
inv-random
[@0: The dog is blue.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "blue" "-")
The lion chases the lion.
Unknown
random
[@0: The lion chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "lion" "+")
The tiger does not chase the lion.
Unknown
inv-random
[@0: The tiger chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "lion" "-")
The cow is big.
Unknown
random
[@0: The cow is big.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "big" "+")
@0: The cow visits the dog.[(triple1)] The dog chases the tiger.[(triple2)] The lion visits the cow.[(triple3)] The tiger visits the dog.[(triple4)] @1: The dog is big.[(((triple4) -> rule7))] @2: The dog is young.[(((((triple4) -> rule7)) -> rule1))] @3: The dog sees the cow.[(((((((triple4) -> rule7)) -> rule1)) -> rule6))]
The cow visits the dog.
("cow" "visits" "dog" "+")
triple1
The dog chases the tiger.
("dog" "chases" "tiger" "+")
triple2
The lion visits the cow.
("lion" "visits" "cow" "+")
triple3
The tiger visits the dog.
("tiger" "visits" "dog" "+")
triple4
The dog is big.
("dog" "is" "big" "+")
((triple4) -> (rule7 % int1))
The dog is big.
("dog" "is" "big" "+")
int1
The dog is young.
("dog" "is" "young" "+")
((((triple4) -> (rule7 % int2))) -> (rule1 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The dog is big.
("dog" "is" "big" "+")
int2
The dog sees the cow.
("dog" "sees" "cow" "+")
((((((triple4) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The dog sees the cow.
("dog" "sees" "cow" "+")
int1
The dog is young.
("dog" "is" "young" "+")
int2
The dog is big.
("dog" "is" "big" "+")
int3