The dog is blue. The dog is not red. The dog is round. All red things are blue. Green, red things are young. All red things are not young. All blue things are green. All young, red things are green. Blue, round things are not red. Green, young things are red. If something is young then it is round.
The dog is blue.
("dog" "is" "blue" "+")
The dog is not red.
("dog" "is" "red" "-")
The dog is round.
("dog" "is" "round" "+")
All red things are blue.
((("something" "is" "red" "+")) -> ("something" "is" "blue" "+"))
Green, red things are young.
((("something" "is" "green" "+") ("something" "is" "red" "+")) -> ("something" "is" "young" "+"))
All red things are not young.
((("something" "is" "red" "+")) -> ("something" "is" "young" "-"))
All blue things are green.
((("something" "is" "blue" "+")) -> ("something" "is" "green" "+"))
All young, red things are green.
((("something" "is" "young" "+") ("something" "is" "red" "+")) -> ("something" "is" "green" "+"))
Blue, round things are not red.
((("something" "is" "blue" "+") ("something" "is" "round" "+")) -> ("something" "is" "red" "-"))
Green, young things are red.
((("something" "is" "green" "+") ("something" "is" "young" "+")) -> ("something" "is" "red" "+"))
If something is young then it is round.
((("something" "is" "young" "+")) -> ("something" "is" "round" "+"))
The dog is round.
True
1
proof
[(triple3)]
("dog" "is" "round" "+")
triple3
The dog is not round.
False
1
inv-proof
[(triple3)]
("dog" "is" "round" "-")
triple3
The dog is green.
True
2
proof
[(((triple1) -> rule4))]
("dog" "is" "green" "+")
((triple1) -> (rule4 % int1))
The dog is green.
("dog" "is" "green" "+")
int1
The dog is not green.
False
2
inv-proof
[(((triple1) -> rule4))]
("dog" "is" "green" "-")
((triple1) -> (rule4 % int1))
The dog is green.
("dog" "is" "green" "+")
int1
The dog is not young.
Unknown
inv-rconc
[@1: The dog is young.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "is" "young" "-")
The dog needs the dog.
Unknown
random
[@0: The dog needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "dog" "+")
The dog does not chase the dog.
Unknown
inv-random
[@0: The dog chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "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 blue.[(triple1)] The dog is not red.[(triple2 OR ((triple1 triple3) -> rule6))] The dog is round.[(triple3)] @1: The dog is green.[(((triple1) -> rule4))]
The dog is blue.
("dog" "is" "blue" "+")
triple1
The dog is not red.
("dog" "is" "red" "-")
triple2
((triple1 triple3) -> (rule6 % int1))
The dog is not red.
("dog" "is" "red" "-")
int1
The dog is round.
("dog" "is" "round" "+")
triple3
The dog is green.
("dog" "is" "green" "+")
((triple1) -> (rule4 % int1))
The dog is green.
("dog" "is" "green" "+")
int1