The cat is nice. All nice things are round. All nice things are green. If something is round then it is nice. Big things are young. All nice things are round. All big things are young. If something is nice and young then it is big. If something is nice and young then it is big.
The cat is nice.
("cat" "is" "nice" "+")
All nice things are round.
((("something" "is" "nice" "+")) -> ("something" "is" "round" "+"))
All nice things are green.
((("something" "is" "nice" "+")) -> ("something" "is" "green" "+"))
If something is round then it is nice.
((("something" "is" "round" "+")) -> ("something" "is" "nice" "+"))
Big things are young.
((("something" "is" "big" "+")) -> ("something" "is" "young" "+"))
All nice things are round.
((("something" "is" "nice" "+")) -> ("something" "is" "round" "+"))
All big things are young.
((("something" "is" "big" "+")) -> ("something" "is" "young" "+"))
If something is nice and young then it is big.
((("something" "is" "nice" "+") ("something" "is" "young" "+")) -> ("something" "is" "big" "+"))
If something is nice and young then it is big.
((("something" "is" "nice" "+") ("something" "is" "young" "+")) -> ("something" "is" "big" "+"))
The cat is nice.
True
1
proof
[(triple1)]
("cat" "is" "nice" "+")
triple1
The cat is not nice.
False
1
inv-proof
[(triple1)]
("cat" "is" "nice" "-")
triple1
The cat is green.
True
2
proof
[(((triple1) -> rule2))]
("cat" "is" "green" "+")
((triple1) -> (rule2 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
The cat is not round.
False
2
inv-proof
[(((triple1) -> rule1) OR ((triple1) -> rule5))]
("cat" "is" "round" "-")
((triple1) -> (rule1 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
((triple1) -> (rule5 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The cat is not big.
Unknown
inv-rconc
[@4: The cat is big.[CWA. Example of deepest failure = (rule7 <- rule4 <- rule8 <- rule6 <- FAIL)]]
("cat" "is" "big" "-")
The cat is young.
Unknown
rconc
[@4: The cat is young.[CWA. Example of deepest failure = (rule4 <- rule7 <- rule6 <- rule8 <- FAIL)]]
("cat" "is" "young" "+")
The cat does not like the cat.
Unknown
inv-random
[@0: The cat likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "cat" "-")
The cat needs the cat.
Unknown
random
[@0: The cat needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "cat" "+")
@0: The cat is nice.[(triple1)] @1: The cat is green.[(((triple1) -> rule2))] The cat is round.[(((triple1) -> rule1) OR ((triple1) -> rule5))]
The cat is nice.
("cat" "is" "nice" "+")
triple1
The cat is green.
("cat" "is" "green" "+")
((triple1) -> (rule2 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
The cat is round.
("cat" "is" "round" "+")
((triple1) -> (rule1 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
((triple1) -> (rule5 % int1))
The cat is round.
("cat" "is" "round" "+")
int1