The cat sees the rabbit. The dog needs the cat. The lion is round. The rabbit needs the cat. If something needs the cat then it needs the dog. If something needs the dog then it chases the rabbit. If something is green and it chases the cat then it sees the rabbit.
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
The dog needs the cat.
("dog" "needs" "cat" "+")
The lion is round.
("lion" "is" "round" "+")
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
If something needs the cat then it needs the dog.
((("something" "needs" "cat" "+")) -> ("something" "needs" "dog" "+"))
If something needs the dog then it chases the rabbit.
((("something" "needs" "dog" "+")) -> ("something" "chases" "rabbit" "+"))
If something is green and it chases the cat then it sees the rabbit.
((("something" "is" "green" "+") ("something" "chases" "cat" "+")) -> ("something" "sees" "rabbit" "+"))
The cat sees the rabbit.
True
1
proof
[(triple1)]
("cat" "sees" "rabbit" "+")
triple1
The lion is not round.
False
1
inv-proof
[(triple3)]
("lion" "is" "round" "-")
triple3
The dog needs the dog.
True
2
proof
[(((triple2) -> rule1))]
("dog" "needs" "dog" "+")
((triple2) -> (rule1 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The dog does not need the dog.
False
2
inv-proof
[(((triple2) -> rule1))]
("dog" "needs" "dog" "-")
((triple2) -> (rule1 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The rabbit chases the rabbit.
True
3
proof
[(((((triple4) -> rule1)) -> rule2))]
("rabbit" "chases" "rabbit" "+")
((((triple4) -> (rule1 % int2))) -> (rule2 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
int2
The dog does not chase the rabbit.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule2))]
("dog" "chases" "rabbit" "-")
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
int1
The dog needs the dog.
("dog" "needs" "dog" "+")
int2
The cat does not need the dog.
Unknown
inv-rconc
[@1: The cat needs the dog.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "needs" "dog" "-")
The lion chases the rabbit.
Unknown
rconc
[@2: The lion chases the rabbit.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("lion" "chases" "rabbit" "+")
The dog does not see the rabbit.
Unknown
inv-rconc
[@1: The dog sees the rabbit.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("dog" "sees" "rabbit" "-")
The cat is round.
Unknown
random
[@0: The cat is round.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "round" "+")
The cat does not need the lion.
Unknown
inv-random
[@0: The cat needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "lion" "-")
The lion sees the dog.
Unknown
random
[@0: The lion sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "dog" "+")
@0: The cat sees the rabbit.[(triple1)] The dog needs the cat.[(triple2)] The lion is round.[(triple3)] The rabbit needs the cat.[(triple4)] @1: The dog needs the dog.[(((triple2) -> rule1))] The rabbit needs the dog.[(((triple4) -> rule1))] @2: The dog chases the rabbit.[(((((triple2) -> rule1)) -> rule2))] The rabbit chases the rabbit.[(((((triple4) -> rule1)) -> rule2))]
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
triple1
The dog needs the cat.
("dog" "needs" "cat" "+")
triple2
The lion is round.
("lion" "is" "round" "+")
triple3
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
triple4
The dog needs the dog.
("dog" "needs" "dog" "+")
((triple2) -> (rule1 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
((triple4) -> (rule1 % int1))
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
int1
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
int1
The dog needs the dog.
("dog" "needs" "dog" "+")
int2
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
((((triple4) -> (rule1 % int2))) -> (rule2 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
int2