The dog is big. The dog is cold. The dog is nice. The dog is round. The dog is young. If someone is young then they are round. All young people are big.
The dog is big.
("dog" "is" "big" "+")
The dog is cold.
("dog" "is" "cold" "+")
The dog is nice.
("dog" "is" "nice" "+")
The dog is round.
("dog" "is" "round" "+")
The dog is young.
("dog" "is" "young" "+")
If someone is young then they are round.
((("someone" "is" "young" "+")) -> ("someone" "is" "round" "+"))
All young people are big.
((("someone" "is" "young" "+")) -> ("someone" "is" "big" "+"))
The dog is big.
True
1
proof
[(triple1 OR ((triple5) -> rule2))]
("dog" "is" "big" "+")
triple1
((triple5) -> (rule2 % int1))
The dog is big.
("dog" "is" "big" "+")
int1
The dog is not big.
False
1
inv-proof
[(triple1 OR ((triple5) -> rule2))]
("dog" "is" "big" "-")
triple1
((triple5) -> (rule2 % int1))
The dog is big.
("dog" "is" "big" "+")
int1
The dog does not visit the dog.
Unknown
inv-random
[@0: The dog visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "dog" "-")
The dog sees the dog.
Unknown
random
[@0: The dog sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "dog" "+")
@0: The dog is big.[(triple1 OR ((triple5) -> rule2))] The dog is cold.[(triple2)] The dog is nice.[(triple3)] The dog is round.[(triple4 OR ((triple5) -> rule1))] The dog is young.[(triple5)]
The dog is big.
("dog" "is" "big" "+")
triple1
((triple5) -> (rule2 % int1))
The dog is big.
("dog" "is" "big" "+")
int1
The dog is cold.
("dog" "is" "cold" "+")
triple2
The dog is nice.
("dog" "is" "nice" "+")
triple3
The dog is round.
("dog" "is" "round" "+")
triple4
((triple5) -> (rule1 % int1))
The dog is round.
("dog" "is" "round" "+")
int1
The dog is young.
("dog" "is" "young" "+")
triple5