The cow does not chase the dog. The cow eats the dog. The dog chases the cow. The dog chases the tiger. The dog does not need the cow. The tiger does not chase the dog. The tiger is big. Round people are nice. If someone chases the tiger then the tiger is round.
The cow does not chase the dog.
("cow" "chases" "dog" "-")
The cow eats the dog.
("cow" "eats" "dog" "+")
The dog chases the cow.
("dog" "chases" "cow" "+")
The dog chases the tiger.
("dog" "chases" "tiger" "+")
The dog does not need the cow.
("dog" "needs" "cow" "-")
The tiger does not chase the dog.
("tiger" "chases" "dog" "-")
The tiger is big.
("tiger" "is" "big" "+")
Round people are nice.
((("someone" "is" "round" "+")) -> ("someone" "is" "nice" "+"))
If someone chases the tiger then the tiger is round.
((("someone" "chases" "tiger" "+")) -> ("tiger" "is" "round" "+"))
The tiger is big.
True
1
proof
[(triple7)]
("tiger" "is" "big" "+")
triple7
The cow does not eat the dog.
False
1
inv-proof
[(triple2)]
("cow" "eats" "dog" "-")
triple2
The tiger is round.
True
2
proof
[(((triple4) -> rule2))]
("tiger" "is" "round" "+")
((triple4) -> (rule2 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The tiger is not round.
False
2
inv-proof
[(((triple4) -> rule2))]
("tiger" "is" "round" "-")
((triple4) -> (rule2 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The tiger is nice.
True
3
proof
[(((((triple4) -> rule2)) -> rule1))]
("tiger" "is" "nice" "+")
((((triple4) -> (rule2 % int2))) -> (rule1 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
The tiger is round.
("tiger" "is" "round" "+")
int2
The tiger is not nice.
False
3
inv-proof
[(((((triple4) -> rule2)) -> rule1))]
("tiger" "is" "nice" "-")
((((triple4) -> (rule2 % int2))) -> (rule1 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
The tiger is round.
("tiger" "is" "round" "+")
int2
The dog is not nice.
Unknown
inv-rconc
[@1: The dog is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "is" "nice" "-")
The cow is nice.
Unknown
rconc
[@1: The cow is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "is" "nice" "+")
The tiger does not need the tiger.
Unknown
inv-random
[@0: The tiger needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "tiger" "-")
The tiger is kind.
Unknown
random
[@0: The tiger is kind.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "kind" "+")
The cow does not chase the tiger.
Unknown
inv-random
[@0: The cow chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "tiger" "-")
The dog chases the dog.
Unknown
random
[@0: The dog chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "dog" "+")
@0: The cow does not chase the dog.[(triple1)] The cow eats the dog.[(triple2)] The dog chases the cow.[(triple3)] The dog chases the tiger.[(triple4)] The dog does not need the cow.[(triple5)] The tiger does not chase the dog.[(triple6)] The tiger is big.[(triple7)] @1: The tiger is round.[(((triple4) -> rule2))] @2: The tiger is nice.[(((((triple4) -> rule2)) -> rule1))]
The cow does not chase the dog.
("cow" "chases" "dog" "-")
triple1
The cow eats the dog.
("cow" "eats" "dog" "+")
triple2
The dog chases the cow.
("dog" "chases" "cow" "+")
triple3
The dog chases the tiger.
("dog" "chases" "tiger" "+")
triple4
The dog does not need the cow.
("dog" "needs" "cow" "-")
triple5
The tiger does not chase the dog.
("tiger" "chases" "dog" "-")
triple6
The tiger is big.
("tiger" "is" "big" "+")
triple7
The tiger is round.
("tiger" "is" "round" "+")
((triple4) -> (rule2 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
((((triple4) -> (rule2 % int2))) -> (rule1 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
The tiger is round.
("tiger" "is" "round" "+")
int2