The cat does not like the tiger. The tiger likes the cat. The tiger needs the cat. If someone is blue and cold then they are not round. Cold people are blue. If someone visits the tiger then they visit the cat. If someone likes the cat and the cat needs the tiger then the tiger visits the cat. If someone likes the cat and they need the tiger then the tiger likes the cat. If the tiger is not rough and the tiger does not need the cat then the tiger does not like the cat. If someone needs the cat then the cat visits the tiger. If someone visits the cat and the cat visits the tiger then the tiger is kind.
The cat does not like the tiger.
("cat" "likes" "tiger" "-")
The tiger likes the cat.
("tiger" "likes" "cat" "+")
The tiger needs the cat.
("tiger" "needs" "cat" "+")
If someone is blue and cold then they are not round.
((("someone" "is" "blue" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "round" "-"))
Cold people are blue.
((("someone" "is" "cold" "+")) -> ("someone" "is" "blue" "+"))
If someone visits the tiger then they visit the cat.
((("someone" "visits" "tiger" "+")) -> ("someone" "visits" "cat" "+"))
If someone likes the cat and the cat needs the tiger then the tiger visits the cat.
((("someone" "likes" "cat" "+") ("cat" "needs" "tiger" "+")) -> ("tiger" "visits" "cat" "+"))
If someone likes the cat and they need the tiger then the tiger likes the cat.
((("someone" "likes" "cat" "+") ("someone" "needs" "tiger" "+")) -> ("tiger" "likes" "cat" "+"))
If the tiger is not rough and the tiger does not need the cat then the tiger does not like the cat.
((("tiger" "is" "rough" "~") ("tiger" "needs" "cat" "~")) -> ("tiger" "likes" "cat" "-"))
If someone needs the cat then the cat visits the tiger.
((("someone" "needs" "cat" "+")) -> ("cat" "visits" "tiger" "+"))
If someone visits the cat and the cat visits the tiger then the tiger is kind.
((("someone" "visits" "cat" "+") ("cat" "visits" "tiger" "+")) -> ("tiger" "is" "kind" "+"))
The cat does not like the tiger.
True
1
proof
[(triple1)]
("cat" "likes" "tiger" "-")
triple1
The tiger does not like the cat.
False
1
inv-proof
[(triple2)]
("tiger" "likes" "cat" "-")
triple2
The cat visits the tiger.
True
2
proof
[(((triple3) -> rule7))]
("cat" "visits" "tiger" "+")
((triple3) -> (rule7 % int1))
The cat visits the tiger.
("cat" "visits" "tiger" "+")
int1
The cat does not visit the tiger.
False
2
inv-proof
[(((triple3) -> rule7))]
("cat" "visits" "tiger" "-")
((triple3) -> (rule7 % int1))
The cat visits the tiger.
("cat" "visits" "tiger" "+")
int1
The cat visits the cat.
True
3
proof
[(((((triple3) -> rule7)) -> rule3))]
("cat" "visits" "cat" "+")
((((triple3) -> (rule7 % int2))) -> (rule3 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The cat visits the tiger.
("cat" "visits" "tiger" "+")
int2
The cat does not visit the cat.
False
3
inv-proof
[(((((triple3) -> rule7)) -> rule3))]
("cat" "visits" "cat" "-")
((((triple3) -> (rule7 % int2))) -> (rule3 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The cat visits the tiger.
("cat" "visits" "tiger" "+")
int2
The tiger is kind.
True
6
proof
[(((((((triple3) -> rule7)) -> rule3) ((triple3) -> rule7)) -> rule8))]
("tiger" "is" "kind" "+")
((((((triple3) -> (rule7 % int3))) -> (rule3 % int2)) ((triple3) -> (rule7 % int3))) -> (rule8 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The cat visits the cat.
("cat" "visits" "cat" "+")
int2
The cat visits the tiger.
("cat" "visits" "tiger" "+")
int3
The tiger is not kind.
False
6
inv-proof
[(((((((triple3) -> rule7)) -> rule3) ((triple3) -> rule7)) -> rule8))]
("tiger" "is" "kind" "-")
((((((triple3) -> (rule7 % int3))) -> (rule3 % int2)) ((triple3) -> (rule7 % int3))) -> (rule8 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The cat visits the cat.
("cat" "visits" "cat" "+")
int2
The cat visits the tiger.
("cat" "visits" "tiger" "+")
int3
The tiger is not blue.
Unknown
inv-rconc
[@1: The tiger is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "is" "blue" "-")
The tiger visits the cat.
Unknown
rconc
[@1: The tiger visits the cat.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "visits" "cat" "+")
The cat is not blue.
Unknown
inv-rconc
[@1: The cat is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "is" "blue" "-")
The tiger is round.
Unknown
random
[@0: The tiger is round.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "round" "+")
The tiger is not cold.
Unknown
inv-random
[@0: The tiger is cold.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "cold" "-")
The cat needs the tiger.
Unknown
random
[@0: The cat needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "tiger" "+")
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 cat is round.
Unknown
random
[@0: The cat is round.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "round" "+")
@0: The cat does not like the tiger.[(triple1)] The tiger likes the cat.[(triple2)] The tiger needs the cat.[(triple3)] @1: The cat visits the tiger.[(((triple3) -> rule7))] @2: The cat visits the cat.[(((((triple3) -> rule7)) -> rule3))] @3: The tiger is kind.[(((((((triple3) -> rule7)) -> rule3) ((triple3) -> rule7)) -> rule8))]
The cat does not like the tiger.
("cat" "likes" "tiger" "-")
triple1
The tiger likes the cat.
("tiger" "likes" "cat" "+")
triple2
The tiger needs the cat.
("tiger" "needs" "cat" "+")
triple3
The cat visits the tiger.
("cat" "visits" "tiger" "+")
((triple3) -> (rule7 % int1))
The cat visits the tiger.
("cat" "visits" "tiger" "+")
int1
The cat visits the cat.
("cat" "visits" "cat" "+")
((((triple3) -> (rule7 % int2))) -> (rule3 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The cat visits the tiger.
("cat" "visits" "tiger" "+")
int2
The tiger is kind.
("tiger" "is" "kind" "+")
((((((triple3) -> (rule7 % int3))) -> (rule3 % int2)) ((triple3) -> (rule7 % int3))) -> (rule8 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The cat visits the cat.
("cat" "visits" "cat" "+")
int2
The cat visits the tiger.
("cat" "visits" "tiger" "+")
int3