The cow sees the lion. The cow visits the squirrel. The dog is red. The lion is young. The lion visits the squirrel. The squirrel visits the cow. The squirrel visits the dog. All cold things are nice. Red things are cold. If something eats the lion and it is not red then the lion is young. If something eats the dog and it does not see the squirrel then the squirrel visits the dog. If the cow eats the dog and the dog is red then the dog is not rough. If something eats the lion then the lion eats the dog. All nice things are rough. If something visits the dog and it is not cold then it is rough.
The cow sees the lion.
("cow" "sees" "lion" "+")
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
The dog is red.
("dog" "is" "red" "+")
The lion is young.
("lion" "is" "young" "+")
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
All cold things are nice.
((("something" "is" "cold" "+")) -> ("something" "is" "nice" "+"))
Red things are cold.
((("something" "is" "red" "+")) -> ("something" "is" "cold" "+"))
If something eats the lion and it is not red then the lion is young.
((("something" "eats" "lion" "+") ("something" "is" "red" "~")) -> ("lion" "is" "young" "+"))
If something eats the dog and it does not see the squirrel then the squirrel visits the dog.
((("something" "eats" "dog" "+") ("something" "sees" "squirrel" "~")) -> ("squirrel" "visits" "dog" "+"))
If the cow eats the dog and the dog is red then the dog is not rough.
((("cow" "eats" "dog" "+") ("dog" "is" "red" "+")) -> ("dog" "is" "rough" "-"))
If something eats the lion then the lion eats the dog.
((("something" "eats" "lion" "+")) -> ("lion" "eats" "dog" "+"))
All nice things are rough.
((("something" "is" "nice" "+")) -> ("something" "is" "rough" "+"))
If something visits the dog and it is not cold then it is rough.
((("something" "visits" "dog" "+") ("something" "is" "cold" "~")) -> ("something" "is" "rough" "+"))
The lion visits the squirrel.
True
1
proof
[(triple5)]
("lion" "visits" "squirrel" "+")
triple5
The squirrel does not visit the dog.
False
1
inv-proof
[(triple7)]
("squirrel" "visits" "dog" "-")
triple7
The dog is cold.
True
2
proof
[(((triple3) -> rule2))]
("dog" "is" "cold" "+")
((triple3) -> (rule2 % int1))
The dog is cold.
("dog" "is" "cold" "+")
int1
The dog is not cold.
False
2
inv-proof
[(((triple3) -> rule2))]
("dog" "is" "cold" "-")
((triple3) -> (rule2 % int1))
The dog is cold.
("dog" "is" "cold" "+")
int1
The dog is nice.
True
3
proof
[(((((triple3) -> rule2)) -> rule1))]
("dog" "is" "nice" "+")
((((triple3) -> (rule2 % int2))) -> (rule1 % int1))
The dog is nice.
("dog" "is" "nice" "+")
int1
The dog is cold.
("dog" "is" "cold" "+")
int2
The dog is not nice.
False
3
inv-proof
[(((((triple3) -> rule2)) -> rule1))]
("dog" "is" "nice" "-")
((((triple3) -> (rule2 % int2))) -> (rule1 % int1))
The dog is nice.
("dog" "is" "nice" "+")
int1
The dog is cold.
("dog" "is" "cold" "+")
int2
The dog is rough.
True
4
proof
[(((((((triple3) -> rule2)) -> rule1)) -> rule7))]
("dog" "is" "rough" "+")
((((((triple3) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The dog is nice.
("dog" "is" "nice" "+")
int2
The dog is cold.
("dog" "is" "cold" "+")
int3
The dog is not rough.
False
4
inv-proof
[(((((((triple3) -> rule2)) -> rule1)) -> rule7))]
("dog" "is" "rough" "-")
((((((triple3) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The dog is nice.
("dog" "is" "nice" "+")
int2
The dog is cold.
("dog" "is" "cold" "+")
int3
The squirrel is not nice.
Unknown
inv-rconc
[@2: The squirrel is nice.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("squirrel" "is" "nice" "-")
The lion eats the dog.
Unknown
rconc
[@1: The lion eats the dog.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("lion" "eats" "dog" "+")
The lion is not cold.
Unknown
inv-rconc
[@1: The lion is cold.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "is" "cold" "-")
The cow is nice.
Unknown
rconc
[@2: The cow is nice.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("cow" "is" "nice" "+")
The dog does not visit the cow.
Unknown
inv-random
[@0: The dog visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "cow" "-")
The cow is young.
Unknown
random
[@0: The cow is young.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "young" "+")
The cow does not eat the lion.
Unknown
inv-random
[@0: The cow eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "lion" "-")
The cow sees the cow.
Unknown
random
[@0: The cow sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "cow" "+")
@0: The cow sees the lion.[(triple1)] The cow visits the squirrel.[(triple2)] The dog is red.[(triple3)] The lion is young.[(triple4)] The lion visits the squirrel.[(triple5)] The squirrel visits the cow.[(triple6)] The squirrel visits the dog.[(triple7)] @1: The dog is cold.[(((triple3) -> rule2))] @2: The dog is nice.[(((((triple3) -> rule2)) -> rule1))] @3: The dog is rough.[(((((((triple3) -> rule2)) -> rule1)) -> rule7))]
The cow sees the lion.
("cow" "sees" "lion" "+")
triple1
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
triple2
The dog is red.
("dog" "is" "red" "+")
triple3
The lion is young.
("lion" "is" "young" "+")
triple4
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
triple5
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
triple6
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
triple7
The dog is cold.
("dog" "is" "cold" "+")
((triple3) -> (rule2 % int1))
The dog is cold.
("dog" "is" "cold" "+")
int1
The dog is nice.
("dog" "is" "nice" "+")
((((triple3) -> (rule2 % int2))) -> (rule1 % int1))
The dog is nice.
("dog" "is" "nice" "+")
int1
The dog is cold.
("dog" "is" "cold" "+")
int2
The dog is rough.
("dog" "is" "rough" "+")
((((((triple3) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The dog is nice.
("dog" "is" "nice" "+")
int2
The dog is cold.
("dog" "is" "cold" "+")
int3