The cow is kind. The cow is nice. The cow visits the dog. The cow visits the squirrel. The dog chases the tiger. The dog needs the cow. The dog visits the tiger. The squirrel is cold. The squirrel is green. The squirrel is kind. The tiger visits the squirrel. If someone is nice and they need the cow then they are cold. If someone needs the dog then the dog is nice. If someone chases the tiger then the tiger visits the dog. If someone visits the tiger and the tiger visits the dog then the tiger visits the cow. If someone visits the cow then they need the dog.
The cow is kind.
("cow" "is" "kind" "+")
The cow is nice.
("cow" "is" "nice" "+")
The cow visits the dog.
("cow" "visits" "dog" "+")
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
The dog chases the tiger.
("dog" "chases" "tiger" "+")
The dog needs the cow.
("dog" "needs" "cow" "+")
The dog visits the tiger.
("dog" "visits" "tiger" "+")
The squirrel is cold.
("squirrel" "is" "cold" "+")
The squirrel is green.
("squirrel" "is" "green" "+")
The squirrel is kind.
("squirrel" "is" "kind" "+")
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
If someone is nice and they need the cow then they are cold.
((("someone" "is" "nice" "+") ("someone" "needs" "cow" "+")) -> ("someone" "is" "cold" "+"))
If someone needs the dog then the dog is nice.
((("someone" "needs" "dog" "+")) -> ("dog" "is" "nice" "+"))
If someone chases the tiger then the tiger visits the dog.
((("someone" "chases" "tiger" "+")) -> ("tiger" "visits" "dog" "+"))
If someone visits the tiger and the tiger visits the dog then the tiger visits the cow.
((("someone" "visits" "tiger" "+") ("tiger" "visits" "dog" "+")) -> ("tiger" "visits" "cow" "+"))
If someone visits the cow then they need the dog.
((("someone" "visits" "cow" "+")) -> ("someone" "needs" "dog" "+"))
The dog needs the cow.
True
1
proof
[(triple6)]
("dog" "needs" "cow" "+")
triple6
The dog does not need the cow.
False
1
inv-proof
[(triple6)]
("dog" "needs" "cow" "-")
triple6
The tiger visits the dog.
True
2
proof
[(((triple5) -> rule3))]
("tiger" "visits" "dog" "+")
((triple5) -> (rule3 % int1))
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int1
The tiger does not visit the dog.
False
2
inv-proof
[(((triple5) -> rule3))]
("tiger" "visits" "dog" "-")
((triple5) -> (rule3 % int1))
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int1
The tiger visits the cow.
True
4
proof
[(((triple7 ((triple5) -> rule3)) -> rule4))]
("tiger" "visits" "cow" "+")
((triple7 ((triple5) -> (rule3 % int2))) -> (rule4 % int1))
The tiger visits the cow.
("tiger" "visits" "cow" "+")
int1
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int2
The tiger does not visit the cow.
False
4
inv-proof
[(((triple7 ((triple5) -> rule3)) -> rule4))]
("tiger" "visits" "cow" "-")
((triple7 ((triple5) -> (rule3 % int2))) -> (rule4 % int1))
The tiger visits the cow.
("tiger" "visits" "cow" "+")
int1
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int2
The tiger needs the dog.
True
5
proof
[(((((triple7 ((triple5) -> rule3)) -> rule4)) -> rule5))]
("tiger" "needs" "dog" "+")
((((triple7 ((triple5) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The tiger needs the dog.
("tiger" "needs" "dog" "+")
int1
The tiger visits the cow.
("tiger" "visits" "cow" "+")
int2
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int3
The tiger does not need the dog.
False
5
inv-proof
[(((((triple7 ((triple5) -> rule3)) -> rule4)) -> rule5))]
("tiger" "needs" "dog" "-")
((((triple7 ((triple5) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The tiger needs the dog.
("tiger" "needs" "dog" "+")
int1
The tiger visits the cow.
("tiger" "visits" "cow" "+")
int2
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int3
The dog is nice.
True
6
proof
[(((((((triple7 ((triple5) -> rule3)) -> rule4)) -> rule5)) -> rule2))]
("dog" "is" "nice" "+")
((((((triple7 ((triple5) -> (rule3 % int4))) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
The dog is nice.
("dog" "is" "nice" "+")
int1
The tiger needs the dog.
("tiger" "needs" "dog" "+")
int2
The tiger visits the cow.
("tiger" "visits" "cow" "+")
int3
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int4
The dog is not nice.
False
6
inv-proof
[(((((((triple7 ((triple5) -> rule3)) -> rule4)) -> rule5)) -> rule2))]
("dog" "is" "nice" "-")
((((((triple7 ((triple5) -> (rule3 % int4))) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
The dog is nice.
("dog" "is" "nice" "+")
int1
The tiger needs the dog.
("tiger" "needs" "dog" "+")
int2
The tiger visits the cow.
("tiger" "visits" "cow" "+")
int3
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int4
The dog is cold.
True
8
proof
[(((((((((triple7 ((triple5) -> rule3)) -> rule4)) -> rule5)) -> rule2) triple6) -> rule1))]
("dog" "is" "cold" "+")
((((((((triple7 ((triple5) -> (rule3 % int5))) -> (rule4 % int4))) -> (rule5 % int3))) -> (rule2 % int2)) triple6) -> (rule1 % int1))
The dog is cold.
("dog" "is" "cold" "+")
int1
The dog is nice.
("dog" "is" "nice" "+")
int2
The tiger needs the dog.
("tiger" "needs" "dog" "+")
int3
The tiger visits the cow.
("tiger" "visits" "cow" "+")
int4
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int5
The dog is not cold.
False
8
inv-proof
[(((((((((triple7 ((triple5) -> rule3)) -> rule4)) -> rule5)) -> rule2) triple6) -> rule1))]
("dog" "is" "cold" "-")
((((((((triple7 ((triple5) -> (rule3 % int5))) -> (rule4 % int4))) -> (rule5 % int3))) -> (rule2 % int2)) triple6) -> (rule1 % int1))
The dog is cold.
("dog" "is" "cold" "+")
int1
The dog is nice.
("dog" "is" "nice" "+")
int2
The tiger needs the dog.
("tiger" "needs" "dog" "+")
int3
The tiger visits the cow.
("tiger" "visits" "cow" "+")
int4
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int5
The dog does not need the dog.
Unknown
inv-rconc
[@1: The dog needs the dog.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("dog" "needs" "dog" "-")
The tiger is cold.
Unknown
rconc
[@1: The tiger is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "is" "cold" "+")
The cow does not need the dog.
Unknown
inv-rconc
[@1: The cow needs the dog.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cow" "needs" "dog" "-")
The squirrel needs the dog.
Unknown
rconc
[@1: The squirrel needs the dog.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("squirrel" "needs" "dog" "+")
The cow is not cold.
Unknown
inv-rconc
[@1: The cow is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "is" "cold" "-")
The cow is green.
Unknown
random
[@0: The cow is green.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "green" "+")
The tiger is not nice.
Unknown
inv-random
[@0: The tiger is nice.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "nice" "-")
The tiger visits the tiger.
Unknown
random
[@0: The tiger visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "tiger" "+")
The squirrel does not need the cow.
Unknown
inv-random
[@0: The squirrel needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "cow" "-")
The dog is green.
Unknown
random
[@0: The dog is green.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "green" "+")
The tiger is not green.
Unknown
inv-random
[@0: The tiger is green.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "green" "-")
The dog visits the squirrel.
Unknown
random
[@0: The dog visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "squirrel" "+")
@0: The cow is kind.[(triple1)] The cow is nice.[(triple2)] The cow visits the dog.[(triple3)] The cow visits the squirrel.[(triple4)] The dog chases the tiger.[(triple5)] The dog needs the cow.[(triple6)] The dog visits the tiger.[(triple7)] The squirrel is cold.[(triple8)] The squirrel is green.[(triple9)] The squirrel is kind.[(triple10)] The tiger visits the squirrel.[(triple11)] @1: The tiger visits the dog.[(((triple5) -> rule3))] @2: The tiger visits the cow.[(((triple7 ((triple5) -> rule3)) -> rule4))] @3: The tiger needs the dog.[(((((triple7 ((triple5) -> rule3)) -> rule4)) -> rule5))] @4: The dog is nice.[(((((((triple7 ((triple5) -> rule3)) -> rule4)) -> rule5)) -> rule2))] @5: The dog is cold.[(((((((((triple7 ((triple5) -> rule3)) -> rule4)) -> rule5)) -> rule2) triple6) -> rule1))]
The cow is kind.
("cow" "is" "kind" "+")
triple1
The cow is nice.
("cow" "is" "nice" "+")
triple2
The cow visits the dog.
("cow" "visits" "dog" "+")
triple3
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
triple4
The dog chases the tiger.
("dog" "chases" "tiger" "+")
triple5
The dog needs the cow.
("dog" "needs" "cow" "+")
triple6
The dog visits the tiger.
("dog" "visits" "tiger" "+")
triple7
The squirrel is cold.
("squirrel" "is" "cold" "+")
triple8
The squirrel is green.
("squirrel" "is" "green" "+")
triple9
The squirrel is kind.
("squirrel" "is" "kind" "+")
triple10
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
triple11
The tiger visits the dog.
("tiger" "visits" "dog" "+")
((triple5) -> (rule3 % int1))
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int1
The tiger visits the cow.
("tiger" "visits" "cow" "+")
((triple7 ((triple5) -> (rule3 % int2))) -> (rule4 % int1))
The tiger visits the cow.
("tiger" "visits" "cow" "+")
int1
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int2
The tiger needs the dog.
("tiger" "needs" "dog" "+")
((((triple7 ((triple5) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The tiger needs the dog.
("tiger" "needs" "dog" "+")
int1
The tiger visits the cow.
("tiger" "visits" "cow" "+")
int2
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int3
The dog is nice.
("dog" "is" "nice" "+")
((((((triple7 ((triple5) -> (rule3 % int4))) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
The dog is nice.
("dog" "is" "nice" "+")
int1
The tiger needs the dog.
("tiger" "needs" "dog" "+")
int2
The tiger visits the cow.
("tiger" "visits" "cow" "+")
int3
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int4
The dog is cold.
("dog" "is" "cold" "+")
((((((((triple7 ((triple5) -> (rule3 % int5))) -> (rule4 % int4))) -> (rule5 % int3))) -> (rule2 % int2)) triple6) -> (rule1 % int1))
The dog is cold.
("dog" "is" "cold" "+")
int1
The dog is nice.
("dog" "is" "nice" "+")
int2
The tiger needs the dog.
("tiger" "needs" "dog" "+")
int3
The tiger visits the cow.
("tiger" "visits" "cow" "+")
int4
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int5