The dog does not chase the squirrel. The lion eats the squirrel. The rabbit eats the squirrel. The squirrel is blue. All blue things are cold. If the lion visits the dog then the dog eats the lion. If something eats the squirrel then it chases the rabbit. If something chases the dog then the dog visits the squirrel. If something is cold then it eats the rabbit. If the lion chases the rabbit then the rabbit visits the dog. If something is cold and it does not visit the squirrel then it chases the lion. If something visits the dog then it chases the lion.
The dog does not chase the squirrel.
("dog" "chases" "squirrel" "-")
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
The squirrel is blue.
("squirrel" "is" "blue" "+")
All blue things are cold.
((("something" "is" "blue" "+")) -> ("something" "is" "cold" "+"))
If the lion visits the dog then the dog eats the lion.
((("lion" "visits" "dog" "+")) -> ("dog" "eats" "lion" "+"))
If something eats the squirrel then it chases the rabbit.
((("something" "eats" "squirrel" "+")) -> ("something" "chases" "rabbit" "+"))
If something chases the dog then the dog visits the squirrel.
((("something" "chases" "dog" "+")) -> ("dog" "visits" "squirrel" "+"))
If something is cold then it eats the rabbit.
((("something" "is" "cold" "+")) -> ("something" "eats" "rabbit" "+"))
If the lion chases the rabbit then the rabbit visits the dog.
((("lion" "chases" "rabbit" "+")) -> ("rabbit" "visits" "dog" "+"))
If something is cold and it does not visit the squirrel then it chases the lion.
((("something" "is" "cold" "+") ("something" "visits" "squirrel" "~")) -> ("something" "chases" "lion" "+"))
If something visits the dog then it chases the lion.
((("something" "visits" "dog" "+")) -> ("something" "chases" "lion" "+"))
The squirrel is blue.
True
1
proof
[(triple4)]
("squirrel" "is" "blue" "+")
triple4
The rabbit does not eat the squirrel.
False
1
inv-proof
[(triple3)]
("rabbit" "eats" "squirrel" "-")
triple3
The squirrel is cold.
True
2
proof
[(((triple4) -> rule1))]
("squirrel" "is" "cold" "+")
((triple4) -> (rule1 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The rabbit does not chase the rabbit.
False
2
inv-proof
[(((triple3) -> rule3))]
("rabbit" "chases" "rabbit" "-")
((triple3) -> (rule3 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The lion is not cold.
Unknown
inv-rconc
[@1: The lion is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "is" "cold" "-")
The rabbit eats the rabbit.
Unknown
rconc
[@2: The rabbit eats the rabbit.[CWA. Example of deepest failure = (rule5 <- rule1 <- FAIL)]]
("rabbit" "eats" "rabbit" "+")
The squirrel does not visit the rabbit.
Unknown
inv-random
[@0: The squirrel visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "rabbit" "-")
The rabbit visits the lion.
Unknown
random
[@0: The rabbit visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "lion" "+")
@0: The dog does not chase the squirrel.[(triple1)] The lion eats the squirrel.[(triple2)] The rabbit eats the squirrel.[(triple3)] The squirrel is blue.[(triple4)] @1: The lion chases the rabbit.[(((triple2) -> rule3))] The rabbit chases the rabbit.[(((triple3) -> rule3))] The squirrel is cold.[(((triple4) -> rule1))] @2: The rabbit visits the dog.[(((((triple2) -> rule3)) -> rule6))] The squirrel eats the rabbit.[(((((triple4) -> rule1)) -> rule5))] @3: The rabbit chases the lion.[(((((((triple2) -> rule3)) -> rule6)) -> rule8))]
The dog does not chase the squirrel.
("dog" "chases" "squirrel" "-")
triple1
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
triple2
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
triple3
The squirrel is blue.
("squirrel" "is" "blue" "+")
triple4
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
((triple2) -> (rule3 % int1))
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
int1
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
((triple3) -> (rule3 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The squirrel is cold.
("squirrel" "is" "cold" "+")
((triple4) -> (rule1 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
((((triple2) -> (rule3 % int2))) -> (rule6 % int1))
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
int1
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
int2
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
((((triple4) -> (rule1 % int2))) -> (rule5 % int1))
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
int1
The squirrel is cold.
("squirrel" "is" "cold" "+")
int2
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
((((((triple2) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
int1
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
int2
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
int3