The dog is green. The dog is red. The dog is rough. The dog is round. The dog is not young. If something is rough then it is red. All red, young things are rough. If the dog is red then the dog is round. All rough things are not young. If the dog is not rough then the dog is not green. If something is red and rough then it is round. If something is green and young then it is not round. Young things are round.
The dog is green.
("dog" "is" "green" "+")
The dog is red.
("dog" "is" "red" "+")
The dog is rough.
("dog" "is" "rough" "+")
The dog is round.
("dog" "is" "round" "+")
The dog is not young.
("dog" "is" "young" "-")
If something is rough then it is red.
((("something" "is" "rough" "+")) -> ("something" "is" "red" "+"))
All red, young things are rough.
((("something" "is" "red" "+") ("something" "is" "young" "+")) -> ("something" "is" "rough" "+"))
If the dog is red then the dog is round.
((("dog" "is" "red" "+")) -> ("dog" "is" "round" "+"))
All rough things are not young.
((("something" "is" "rough" "+")) -> ("something" "is" "young" "-"))
If the dog is not rough then the dog is not green.
((("dog" "is" "rough" "~")) -> ("dog" "is" "green" "-"))
If something is red and rough then it is round.
((("something" "is" "red" "+") ("something" "is" "rough" "+")) -> ("something" "is" "round" "+"))
If something is green and young then it is not round.
((("something" "is" "green" "+") ("something" "is" "young" "+")) -> ("something" "is" "round" "-"))
Young things are round.
((("something" "is" "young" "+")) -> ("something" "is" "round" "+"))
The dog is round.
True
1
proof
[(triple4 OR ((triple2) -> rule3) OR ((triple2 triple3) -> rule6) OR ((((triple3) -> rule1)) -> rule3) OR ((((triple3) -> rule1) triple3) -> rule6))]
("dog" "is" "round" "+")
triple4
((triple2) -> (rule3 % int1))
The dog is round.
("dog" "is" "round" "+")
int1
((triple2 triple3) -> (rule6 % int1))
The dog is round.
("dog" "is" "round" "+")
int1
((((triple3) -> (rule1 % int2))) -> (rule3 % int1))
The dog is round.
("dog" "is" "round" "+")
int1
The dog is red.
("dog" "is" "red" "+")
int2
((((triple3) -> (rule1 % int2)) triple3) -> (rule6 % int1))
The dog is round.
("dog" "is" "round" "+")
int1
The dog is red.
("dog" "is" "red" "+")
int2
The dog is not rough.
False
1
inv-proof
[(triple3)]
("dog" "is" "rough" "-")
triple3
The dog does not need the dog.
Unknown
inv-random
[@0: The dog needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "dog" "-")
The dog chases the dog.
Unknown
random
[@0: The dog chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "dog" "+")
@0: The dog is green.[(triple1)] The dog is not young.[(triple5 OR ((triple3) -> rule4))] The dog is red.[(triple2 OR ((triple3) -> rule1))] The dog is rough.[(triple3)] The dog is round.[(triple4 OR ((triple2) -> rule3) OR ((triple2 triple3) -> rule6) OR ((((triple3) -> rule1)) -> rule3) OR ((((triple3) -> rule1) triple3) -> rule6))]
The dog is green.
("dog" "is" "green" "+")
triple1
The dog is not young.
("dog" "is" "young" "-")
triple5
((triple3) -> (rule4 % int1))
The dog is not young.
("dog" "is" "young" "-")
int1
The dog is red.
("dog" "is" "red" "+")
triple2
((triple3) -> (rule1 % int1))
The dog is red.
("dog" "is" "red" "+")
int1
The dog is rough.
("dog" "is" "rough" "+")
triple3
The dog is round.
("dog" "is" "round" "+")
triple4
((triple2) -> (rule3 % int1))
The dog is round.
("dog" "is" "round" "+")
int1
((triple2 triple3) -> (rule6 % int1))
The dog is round.
("dog" "is" "round" "+")
int1
((((triple3) -> (rule1 % int2))) -> (rule3 % int1))
The dog is round.
("dog" "is" "round" "+")
int1
The dog is red.
("dog" "is" "red" "+")
int2
((((triple3) -> (rule1 % int2)) triple3) -> (rule6 % int1))
The dog is round.
("dog" "is" "round" "+")
int1
The dog is red.
("dog" "is" "red" "+")
int2