The cow is rough. The cow needs the lion. The cow visits the dog. The dog is green. The dog does not need the cow. The dog visits the cow. The lion is not blue. All young things are blue. If something likes the dog then it needs the lion. If something needs the lion then it likes the lion. If something needs the cow and the cow needs the dog then the dog likes the cow. If something likes the cow then it is kind. If something is blue and it needs the cow then it visits the cow. If something visits the dog then the dog needs the lion. If something visits the dog and it does not visit the cow then the dog likes the lion.
The cow is rough.
("cow" "is" "rough" "+")
The cow needs the lion.
("cow" "needs" "lion" "+")
The cow visits the dog.
("cow" "visits" "dog" "+")
The dog is green.
("dog" "is" "green" "+")
The dog does not need the cow.
("dog" "needs" "cow" "-")
The dog visits the cow.
("dog" "visits" "cow" "+")
The lion is not blue.
("lion" "is" "blue" "-")
All young things are blue.
((("something" "is" "young" "+")) -> ("something" "is" "blue" "+"))
If something likes the dog then it needs the lion.
((("something" "likes" "dog" "+")) -> ("something" "needs" "lion" "+"))
If something needs the lion then it likes the lion.
((("something" "needs" "lion" "+")) -> ("something" "likes" "lion" "+"))
If something needs the cow and the cow needs the dog then the dog likes the cow.
((("something" "needs" "cow" "+") ("cow" "needs" "dog" "+")) -> ("dog" "likes" "cow" "+"))
If something likes the cow then it is kind.
((("something" "likes" "cow" "+")) -> ("something" "is" "kind" "+"))
If something is blue and it needs the cow then it visits the cow.
((("something" "is" "blue" "+") ("something" "needs" "cow" "+")) -> ("something" "visits" "cow" "+"))
If something visits the dog then the dog needs the lion.
((("something" "visits" "dog" "+")) -> ("dog" "needs" "lion" "+"))
If something visits the dog and it does not visit the cow then the dog likes the lion.
((("something" "visits" "dog" "+") ("something" "visits" "cow" "~")) -> ("dog" "likes" "lion" "+"))
The dog visits the cow.
True
1
proof
[(triple6)]
("dog" "visits" "cow" "+")
triple6
The cow does not need the lion.
False
1
inv-proof
[(triple2)]
("cow" "needs" "lion" "-")
triple2
The cow likes the lion.
True
2
proof
[(((triple2) -> rule3))]
("cow" "likes" "lion" "+")
((triple2) -> (rule3 % int1))
The cow likes the lion.
("cow" "likes" "lion" "+")
int1
The cow does not like the lion.
False
2
inv-proof
[(((triple2) -> rule3))]
("cow" "likes" "lion" "-")
((triple2) -> (rule3 % int1))
The cow likes the lion.
("cow" "likes" "lion" "+")
int1
The dog likes the lion.
True
3
proof
[(((((triple3) -> rule7)) -> rule3))]
("dog" "likes" "lion" "+")
((((triple3) -> (rule7 % int2))) -> (rule3 % int1))
The dog likes the lion.
("dog" "likes" "lion" "+")
int1
The dog needs the lion.
("dog" "needs" "lion" "+")
int2
The dog does not like the lion.
False
3
inv-proof
[(((((triple3) -> rule7)) -> rule3))]
("dog" "likes" "lion" "-")
((((triple3) -> (rule7 % int2))) -> (rule3 % int1))
The dog likes the lion.
("dog" "likes" "lion" "+")
int1
The dog needs the lion.
("dog" "needs" "lion" "+")
int2
The lion does not visit the cow.
Unknown
inv-rconc
[@1: The lion visits the cow.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("lion" "visits" "cow" "-")
The dog likes the cow.
Unknown
rconc
[@1: The dog likes the cow.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("dog" "likes" "cow" "+")
The dog is not kind.
Unknown
inv-rconc
[@2: The dog is kind.[CWA. Example of deepest failure = (rule5 <- rule4 <- FAIL)]]
("dog" "is" "kind" "-")
The lion visits the lion.
Unknown
random
[@0: The lion visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "lion" "+")
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 rough.[(triple1)] The cow needs the lion.[(triple2)] The cow visits the dog.[(triple3)] The dog does not need the cow.[(triple5)] The dog is green.[(triple4)] The dog visits the cow.[(triple6)] The lion is not blue.[(triple7)] @1: The cow likes the lion.[(((triple2) -> rule3))] The dog needs the lion.[(((triple3) -> rule7))] @2: The dog likes the lion.[(((((triple3) -> rule7)) -> rule3))]
The cow is rough.
("cow" "is" "rough" "+")
triple1
The cow needs the lion.
("cow" "needs" "lion" "+")
triple2
The cow visits the dog.
("cow" "visits" "dog" "+")
triple3
The dog does not need the cow.
("dog" "needs" "cow" "-")
triple5
The dog is green.
("dog" "is" "green" "+")
triple4
The dog visits the cow.
("dog" "visits" "cow" "+")
triple6
The lion is not blue.
("lion" "is" "blue" "-")
triple7
The cow likes the lion.
("cow" "likes" "lion" "+")
((triple2) -> (rule3 % int1))
The cow likes the lion.
("cow" "likes" "lion" "+")
int1
The dog needs the lion.
("dog" "needs" "lion" "+")
((triple3) -> (rule7 % int1))
The dog needs the lion.
("dog" "needs" "lion" "+")
int1
The dog likes the lion.
("dog" "likes" "lion" "+")
((((triple3) -> (rule7 % int2))) -> (rule3 % int1))
The dog likes the lion.
("dog" "likes" "lion" "+")
int1
The dog needs the lion.
("dog" "needs" "lion" "+")
int2