The cow is round. The dog is cold. The dog is kind. The dog likes the cow. The dog does not see the tiger. The dog visits the cow. The tiger is not big. The tiger is kind. The tiger does not see the dog. The tiger visits the cow. If the dog visits the tiger then the dog sees the tiger. If something is rough then it likes the tiger. If something visits the dog then it visits the cow. If something is rough and not cold then it sees the tiger. If something is round and it likes the tiger then it visits the tiger. If something is round then it sees the dog. All round things are rough. If something visits the dog then the dog sees the cow.
The cow is round.
("cow" "is" "round" "+")
The dog is cold.
("dog" "is" "cold" "+")
The dog is kind.
("dog" "is" "kind" "+")
The dog likes the cow.
("dog" "likes" "cow" "+")
The dog does not see the tiger.
("dog" "sees" "tiger" "-")
The dog visits the cow.
("dog" "visits" "cow" "+")
The tiger is not big.
("tiger" "is" "big" "-")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger does not see the dog.
("tiger" "sees" "dog" "-")
The tiger visits the cow.
("tiger" "visits" "cow" "+")
If the dog visits the tiger then the dog sees the tiger.
((("dog" "visits" "tiger" "+")) -> ("dog" "sees" "tiger" "+"))
If something is rough then it likes the tiger.
((("something" "is" "rough" "+")) -> ("something" "likes" "tiger" "+"))
If something visits the dog then it visits the cow.
((("something" "visits" "dog" "+")) -> ("something" "visits" "cow" "+"))
If something is rough and not cold then it sees the tiger.
((("something" "is" "rough" "+") ("something" "is" "cold" "~")) -> ("something" "sees" "tiger" "+"))
If something is round and it likes the tiger then it visits the tiger.
((("something" "is" "round" "+") ("something" "likes" "tiger" "+")) -> ("something" "visits" "tiger" "+"))
If something is round then it sees the dog.
((("something" "is" "round" "+")) -> ("something" "sees" "dog" "+"))
All round things are rough.
((("something" "is" "round" "+")) -> ("something" "is" "rough" "+"))
If something visits the dog then the dog sees the cow.
((("something" "visits" "dog" "+")) -> ("dog" "sees" "cow" "+"))
The dog is cold.
True
1
proof
[(triple2)]
("dog" "is" "cold" "+")
triple2
The dog is not cold.
False
1
inv-proof
[(triple2)]
("dog" "is" "cold" "-")
triple2
The cow sees the dog.
True
2
proof
[(((triple1) -> rule6))]
("cow" "sees" "dog" "+")
((triple1) -> (rule6 % int1))
The cow sees the dog.
("cow" "sees" "dog" "+")
int1
The cow does not see the dog.
False
2
inv-proof
[(((triple1) -> rule6))]
("cow" "sees" "dog" "-")
((triple1) -> (rule6 % int1))
The cow sees the dog.
("cow" "sees" "dog" "+")
int1
The cow likes the tiger.
True
3
proof
[(((((triple1) -> rule7)) -> rule2))]
("cow" "likes" "tiger" "+")
((((triple1) -> (rule7 % int2))) -> (rule2 % int1))
The cow likes the tiger.
("cow" "likes" "tiger" "+")
int1
The cow is rough.
("cow" "is" "rough" "+")
int2
The cow does not like the tiger.
False
3
inv-proof
[(((((triple1) -> rule7)) -> rule2))]
("cow" "likes" "tiger" "-")
((((triple1) -> (rule7 % int2))) -> (rule2 % int1))
The cow likes the tiger.
("cow" "likes" "tiger" "+")
int1
The cow is rough.
("cow" "is" "rough" "+")
int2
The cow visits the tiger.
True
5
proof
[(((triple1 ((((triple1) -> rule7)) -> rule2)) -> rule5))]
("cow" "visits" "tiger" "+")
((triple1 ((((triple1) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The cow visits the tiger.
("cow" "visits" "tiger" "+")
int1
The cow likes the tiger.
("cow" "likes" "tiger" "+")
int2
The cow is rough.
("cow" "is" "rough" "+")
int3
The cow does not visit the tiger.
False
5
inv-proof
[(((triple1 ((((triple1) -> rule7)) -> rule2)) -> rule5))]
("cow" "visits" "tiger" "-")
((triple1 ((((triple1) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The cow visits the tiger.
("cow" "visits" "tiger" "+")
int1
The cow likes the tiger.
("cow" "likes" "tiger" "+")
int2
The cow is rough.
("cow" "is" "rough" "+")
int3
The tiger does not like the tiger.
Unknown
inv-rconc
[@2: The tiger likes the tiger.[CWA. Example of deepest failure = (rule2 <- rule7 <- FAIL)]]
("tiger" "likes" "tiger" "-")
The dog is rough.
Unknown
rconc
[@1: The dog is rough.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("dog" "is" "rough" "+")
The dog does not visit the tiger.
Unknown
inv-rconc
[@1: The dog visits the tiger.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("dog" "visits" "tiger" "-")
The dog likes the tiger.
Unknown
rconc
[@2: The dog likes the tiger.[CWA. Example of deepest failure = (rule2 <- rule7 <- FAIL)]]
("dog" "likes" "tiger" "+")
The tiger does not like the dog.
Unknown
inv-random
[@0: The tiger likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "dog" "-")
The cow visits the dog.
Unknown
random
[@0: The cow visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "dog" "+")
The cow does not like the cow.
Unknown
inv-random
[@0: The cow likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "likes" "cow" "-")
The dog visits the dog.
Unknown
random
[@0: The dog visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "dog" "+")
@0: The cow is round.[(triple1)] The dog does not see the tiger.[(triple5)] The dog is cold.[(triple2)] The dog is kind.[(triple3)] The dog likes the cow.[(triple4)] The dog visits the cow.[(triple6)] The tiger does not see the dog.[(triple9)] The tiger is kind.[(triple8)] The tiger is not big.[(triple7)] The tiger visits the cow.[(triple10)] @1: The cow is rough.[(((triple1) -> rule7))] The cow sees the dog.[(((triple1) -> rule6))] @2: The cow likes the tiger.[(((((triple1) -> rule7)) -> rule2))] @3: The cow visits the tiger.[(((triple1 ((((triple1) -> rule7)) -> rule2)) -> rule5))]
The cow is round.
("cow" "is" "round" "+")
triple1
The dog does not see the tiger.
("dog" "sees" "tiger" "-")
triple5
The dog is cold.
("dog" "is" "cold" "+")
triple2
The dog is kind.
("dog" "is" "kind" "+")
triple3
The dog likes the cow.
("dog" "likes" "cow" "+")
triple4
The dog visits the cow.
("dog" "visits" "cow" "+")
triple6
The tiger does not see the dog.
("tiger" "sees" "dog" "-")
triple9
The tiger is kind.
("tiger" "is" "kind" "+")
triple8
The tiger is not big.
("tiger" "is" "big" "-")
triple7
The tiger visits the cow.
("tiger" "visits" "cow" "+")
triple10
The cow is rough.
("cow" "is" "rough" "+")
((triple1) -> (rule7 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The cow sees the dog.
("cow" "sees" "dog" "+")
((triple1) -> (rule6 % int1))
The cow sees the dog.
("cow" "sees" "dog" "+")
int1
The cow likes the tiger.
("cow" "likes" "tiger" "+")
((((triple1) -> (rule7 % int2))) -> (rule2 % int1))
The cow likes the tiger.
("cow" "likes" "tiger" "+")
int1
The cow is rough.
("cow" "is" "rough" "+")
int2
The cow visits the tiger.
("cow" "visits" "tiger" "+")
((triple1 ((((triple1) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The cow visits the tiger.
("cow" "visits" "tiger" "+")
int1
The cow likes the tiger.
("cow" "likes" "tiger" "+")
int2
The cow is rough.
("cow" "is" "rough" "+")
int3