The cow is big. The cow is blue. The cow sees the dog. The cow visits the dog. The dog sees the cow. The dog sees the squirrel. The dog does not visit the cow. The dog visits the squirrel. The squirrel is big. The squirrel is not young. If something sees the squirrel then it eats the cow. If something is young and it sees the cow then it eats the squirrel. If something is big and green then it does not see the cow. If the dog is green and the squirrel does not see the dog then the squirrel sees the cow. If something is green then it visits the dog. If something eats the squirrel then the squirrel is not kind. If something sees the dog then it is green. All green things are big.
The cow is big.
("cow" "is" "big" "+")
The cow is blue.
("cow" "is" "blue" "+")
The cow sees the dog.
("cow" "sees" "dog" "+")
The cow visits the dog.
("cow" "visits" "dog" "+")
The dog sees the cow.
("dog" "sees" "cow" "+")
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
The dog does not visit the cow.
("dog" "visits" "cow" "-")
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
The squirrel is big.
("squirrel" "is" "big" "+")
The squirrel is not young.
("squirrel" "is" "young" "-")
If something sees the squirrel then it eats the cow.
((("something" "sees" "squirrel" "+")) -> ("something" "eats" "cow" "+"))
If something is young and it sees the cow then it eats the squirrel.
((("something" "is" "young" "+") ("something" "sees" "cow" "+")) -> ("something" "eats" "squirrel" "+"))
If something is big and green then it does not see the cow.
((("something" "is" "big" "+") ("something" "is" "green" "+")) -> ("something" "sees" "cow" "-"))
If the dog is green and the squirrel does not see the dog then the squirrel sees the cow.
((("dog" "is" "green" "+") ("squirrel" "sees" "dog" "~")) -> ("squirrel" "sees" "cow" "+"))
If something is green then it visits the dog.
((("something" "is" "green" "+")) -> ("something" "visits" "dog" "+"))
If something eats the squirrel then the squirrel is not kind.
((("something" "eats" "squirrel" "+")) -> ("squirrel" "is" "kind" "-"))
If something sees the dog then it is green.
((("something" "sees" "dog" "+")) -> ("something" "is" "green" "+"))
All green things are big.
((("something" "is" "green" "+")) -> ("something" "is" "big" "+"))
The cow is big.
True
1
proof
[(triple1 OR ((((triple3) -> rule7)) -> rule8))]
("cow" "is" "big" "+")
triple1
((((triple3) -> (rule7 % int2))) -> (rule8 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The cow is green.
("cow" "is" "green" "+")
int2
The dog does not see the cow.
False
1
inv-proof
[(triple5)]
("dog" "sees" "cow" "-")
triple5
The cow is green.
True
2
proof
[(((triple3) -> rule7))]
("cow" "is" "green" "+")
((triple3) -> (rule7 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow is not green.
False
2
inv-proof
[(((triple3) -> rule7))]
("cow" "is" "green" "-")
((triple3) -> (rule7 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow does not see the cow.
True
4
proof
[(((triple1 ((triple3) -> rule7)) -> rule3) OR ((((((triple3) -> rule7)) -> rule8) ((triple3) -> rule7)) -> rule3))]
("cow" "sees" "cow" "-")
((triple1 ((triple3) -> (rule7 % int2))) -> (rule3 % int1))
The cow does not see the cow.
("cow" "sees" "cow" "-")
int1
The cow is green.
("cow" "is" "green" "+")
int2
((((((triple3) -> (rule7 % int3))) -> (rule8 % int2)) ((triple3) -> (rule7 % int3))) -> (rule3 % int1))
The cow does not see the cow.
("cow" "sees" "cow" "-")
int1
The cow is big.
("cow" "is" "big" "+")
int2
The cow is green.
("cow" "is" "green" "+")
int3
The cow sees the cow.
False
4
inv-proof
[(((triple1 ((triple3) -> rule7)) -> rule3) OR ((((((triple3) -> rule7)) -> rule8) ((triple3) -> rule7)) -> rule3))]
("cow" "sees" "cow" "+")
((triple1 ((triple3) -> (rule7 % int2))) -> (rule3 % int1))
The cow does not see the cow.
("cow" "sees" "cow" "-")
int1
The cow is green.
("cow" "is" "green" "+")
int2
((((((triple3) -> (rule7 % int3))) -> (rule8 % int2)) ((triple3) -> (rule7 % int3))) -> (rule3 % int1))
The cow does not see the cow.
("cow" "sees" "cow" "-")
int1
The cow is big.
("cow" "is" "big" "+")
int2
The cow is green.
("cow" "is" "green" "+")
int3
The dog is not green.
Unknown
inv-rconc
[@1: The dog is green.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("dog" "is" "green" "-")
The cow eats the squirrel.
Unknown
rconc
[@1: The cow eats the squirrel.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "eats" "squirrel" "+")
The squirrel is not green.
Unknown
inv-rconc
[@1: The squirrel is green.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("squirrel" "is" "green" "-")
The squirrel is blue.
Unknown
random
[@0: The squirrel is blue.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "blue" "+")
The dog is not blue.
Unknown
inv-random
[@0: The dog is blue.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "blue" "-")
The cow is kind.
Unknown
random
[@0: The cow is kind.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "kind" "+")
@0: The cow is big.[(triple1 OR ((((triple3) -> rule7)) -> rule8))] The cow is blue.[(triple2)] The cow sees the dog.[(triple3)] The cow visits the dog.[(triple4 OR ((((triple3) -> rule7)) -> rule5))] The dog does not visit the cow.[(triple7)] The dog sees the cow.[(triple5)] The dog sees the squirrel.[(triple6)] The dog visits the squirrel.[(triple8)] The squirrel is big.[(triple9)] The squirrel is not young.[(triple10)] @1: The cow is green.[(((triple3) -> rule7))] The dog eats the cow.[(((triple6) -> rule1))] @2: The cow does not see the cow.[(((triple1 ((triple3) -> rule7)) -> rule3) OR ((((((triple3) -> rule7)) -> rule8) ((triple3) -> rule7)) -> rule3))]
The cow is big.
("cow" "is" "big" "+")
triple1
((((triple3) -> (rule7 % int2))) -> (rule8 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The cow is green.
("cow" "is" "green" "+")
int2
The cow is blue.
("cow" "is" "blue" "+")
triple2
The cow sees the dog.
("cow" "sees" "dog" "+")
triple3
The cow visits the dog.
("cow" "visits" "dog" "+")
triple4
((((triple3) -> (rule7 % int2))) -> (rule5 % int1))
The cow visits the dog.
("cow" "visits" "dog" "+")
int1
The cow is green.
("cow" "is" "green" "+")
int2
The dog does not visit the cow.
("dog" "visits" "cow" "-")
triple7
The dog sees the cow.
("dog" "sees" "cow" "+")
triple5
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
triple6
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
triple8
The squirrel is big.
("squirrel" "is" "big" "+")
triple9
The squirrel is not young.
("squirrel" "is" "young" "-")
triple10
The cow is green.
("cow" "is" "green" "+")
((triple3) -> (rule7 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The dog eats the cow.
("dog" "eats" "cow" "+")
((triple6) -> (rule1 % int1))
The dog eats the cow.
("dog" "eats" "cow" "+")
int1
The cow does not see the cow.
("cow" "sees" "cow" "-")
((triple1 ((triple3) -> (rule7 % int2))) -> (rule3 % int1))
The cow does not see the cow.
("cow" "sees" "cow" "-")
int1
The cow is green.
("cow" "is" "green" "+")
int2
((((((triple3) -> (rule7 % int3))) -> (rule8 % int2)) ((triple3) -> (rule7 % int3))) -> (rule3 % int1))
The cow does not see the cow.
("cow" "sees" "cow" "-")
int1
The cow is big.
("cow" "is" "big" "+")
int2
The cow is green.
("cow" "is" "green" "+")
int3