The cow is red. The dog is big. The mouse chases the dog. If something is red then it sees the mouse. If something chases the dog then it sees the dog. If something is red then it sees the cow. If something visits the cow and it sees the dog then the cow visits the mouse. If something chases the cow then it is not nice. If something sees the cow and it is not big then it is nice. If something sees the mouse then the mouse chases the cow. If something visits the cow then it is red.
The cow is red.
("cow" "is" "red" "+")
The dog is big.
("dog" "is" "big" "+")
The mouse chases the dog.
("mouse" "chases" "dog" "+")
If something is red then it sees the mouse.
((("something" "is" "red" "+")) -> ("something" "sees" "mouse" "+"))
If something chases the dog then it sees the dog.
((("something" "chases" "dog" "+")) -> ("something" "sees" "dog" "+"))
If something is red then it sees the cow.
((("something" "is" "red" "+")) -> ("something" "sees" "cow" "+"))
If something visits the cow and it sees the dog then the cow visits the mouse.
((("something" "visits" "cow" "+") ("something" "sees" "dog" "+")) -> ("cow" "visits" "mouse" "+"))
If something chases the cow then it is not nice.
((("something" "chases" "cow" "+")) -> ("something" "is" "nice" "-"))
If something sees the cow and it is not big then it is nice.
((("something" "sees" "cow" "+") ("something" "is" "big" "~")) -> ("something" "is" "nice" "+"))
If something sees the mouse then the mouse chases the cow.
((("something" "sees" "mouse" "+")) -> ("mouse" "chases" "cow" "+"))
If something visits the cow then it is red.
((("something" "visits" "cow" "+")) -> ("something" "is" "red" "+"))
The cow is red.
True
1
proof
[(triple1)]
("cow" "is" "red" "+")
triple1
The dog is not big.
False
1
inv-proof
[(triple2)]
("dog" "is" "big" "-")
triple2
The cow sees the cow.
True
2
proof
[(((triple1) -> rule3))]
("cow" "sees" "cow" "+")
((triple1) -> (rule3 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
The cow does not see the cow.
False
2
inv-proof
[(((triple1) -> rule3))]
("cow" "sees" "cow" "-")
((triple1) -> (rule3 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
The mouse chases the cow.
True
3
proof
[(((((triple1) -> rule1)) -> rule7))]
("mouse" "chases" "cow" "+")
((((triple1) -> (rule1 % int2))) -> (rule7 % int1))
The mouse chases the cow.
("mouse" "chases" "cow" "+")
int1
The cow sees the mouse.
("cow" "sees" "mouse" "+")
int2
The mouse does not chase the cow.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule7))]
("mouse" "chases" "cow" "-")
((((triple1) -> (rule1 % int2))) -> (rule7 % int1))
The mouse chases the cow.
("mouse" "chases" "cow" "+")
int1
The cow sees the mouse.
("cow" "sees" "mouse" "+")
int2
The mouse is not nice.
True
4
proof
[(((((((triple1) -> rule1)) -> rule7)) -> rule5))]
("mouse" "is" "nice" "-")
((((((triple1) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
The mouse is not nice.
("mouse" "is" "nice" "-")
int1
The mouse chases the cow.
("mouse" "chases" "cow" "+")
int2
The cow sees the mouse.
("cow" "sees" "mouse" "+")
int3
The mouse is nice.
False
4
inv-proof
[(((((((triple1) -> rule1)) -> rule7)) -> rule5))]
("mouse" "is" "nice" "+")
((((((triple1) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
The mouse is not nice.
("mouse" "is" "nice" "-")
int1
The mouse chases the cow.
("mouse" "chases" "cow" "+")
int2
The cow sees the mouse.
("cow" "sees" "mouse" "+")
int3
The dog is not red.
Unknown
inv-rconc
[@1: The dog is red.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("dog" "is" "red" "-")
The cow sees the dog.
Unknown
rconc
[@1: The cow sees the dog.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "sees" "dog" "+")
The dog does not see the mouse.
Unknown
inv-rconc
[@2: The dog sees the mouse.[CWA. Example of deepest failure = (rule1 <- rule8 <- FAIL)]]
("dog" "sees" "mouse" "-")
The dog sees the dog.
Unknown
rconc
[@1: The dog sees the dog.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "sees" "dog" "+")
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 mouse visits the mouse.
Unknown
random
[@0: The mouse visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "mouse" "+")
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 cow is cold.
Unknown
random
[@0: The cow is cold.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "cold" "+")
@0: The cow is red.[(triple1)] The dog is big.[(triple2)] The mouse chases the dog.[(triple3)] @1: The cow sees the cow.[(((triple1) -> rule3))] The cow sees the mouse.[(((triple1) -> rule1))] The mouse sees the dog.[(((triple3) -> rule2))] @2: The mouse chases the cow.[(((((triple1) -> rule1)) -> rule7))] @3: The mouse is not nice.[(((((((triple1) -> rule1)) -> rule7)) -> rule5))]
The cow is red.
("cow" "is" "red" "+")
triple1
The dog is big.
("dog" "is" "big" "+")
triple2
The mouse chases the dog.
("mouse" "chases" "dog" "+")
triple3
The cow sees the cow.
("cow" "sees" "cow" "+")
((triple1) -> (rule3 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
The cow sees the mouse.
("cow" "sees" "mouse" "+")
((triple1) -> (rule1 % int1))
The cow sees the mouse.
("cow" "sees" "mouse" "+")
int1
The mouse sees the dog.
("mouse" "sees" "dog" "+")
((triple3) -> (rule2 % int1))
The mouse sees the dog.
("mouse" "sees" "dog" "+")
int1
The mouse chases the cow.
("mouse" "chases" "cow" "+")
((((triple1) -> (rule1 % int2))) -> (rule7 % int1))
The mouse chases the cow.
("mouse" "chases" "cow" "+")
int1
The cow sees the mouse.
("cow" "sees" "mouse" "+")
int2
The mouse is not nice.
("mouse" "is" "nice" "-")
((((((triple1) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
The mouse is not nice.
("mouse" "is" "nice" "-")
int1
The mouse chases the cow.
("mouse" "chases" "cow" "+")
int2
The cow sees the mouse.
("cow" "sees" "mouse" "+")
int3