Dave is green. Dave is kind. Dave is red. Dave is round. Dave is smart. Fiona is blue. Fiona is green. Fiona is red. Fiona is round. Fiona is smart. Fiona is young. Gary is green. Gary is red. Gary is round. Gary is smart. If someone is smart and blue then they are round. All round people are red. All kind people are blue. If Dave is round then Dave is kind. If someone is kind then they are young. All smart, green people are young.
Dave is green.
("Dave" "is" "green" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Fiona is young.
("Fiona" "is" "young" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is smart.
("Gary" "is" "smart" "+")
If someone is smart and blue then they are round.
((("someone" "is" "smart" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "round" "+"))
All round people are red.
((("someone" "is" "round" "+")) -> ("someone" "is" "red" "+"))
All kind people are blue.
((("someone" "is" "kind" "+")) -> ("someone" "is" "blue" "+"))
If Dave is round then Dave is kind.
((("Dave" "is" "round" "+")) -> ("Dave" "is" "kind" "+"))
If someone is kind then they are young.
((("someone" "is" "kind" "+")) -> ("someone" "is" "young" "+"))
All smart, green people are young.
((("someone" "is" "smart" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "young" "+"))
Dave is round.
True
1
proof
[(triple4 OR ((triple5 ((triple2) -> rule3)) -> rule1))]
("Dave" "is" "round" "+")
triple4
((triple5 ((triple2) -> (rule3 % int2))) -> (rule1 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is not green.
False
1
inv-proof
[(triple1)]
("Dave" "is" "green" "-")
triple1
Gary is not blue.
Unknown
inv-rconc
[@1: Gary is blue.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "blue" "-")
Fiona is kind.
Unknown
random
[@0: Fiona is kind.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "kind" "+")
@0: Dave is green.[(triple1)] Dave is kind.[(triple2 OR ((triple4) -> rule4))] Dave is red.[(triple3 OR ((triple4) -> rule2) OR ((((triple5 ((triple2) -> rule3)) -> rule1)) -> rule2))] Dave is round.[(triple4 OR ((triple5 ((triple2) -> rule3)) -> rule1))] Dave is smart.[(triple5)] Fiona is blue.[(triple6)] Fiona is green.[(triple7)] Fiona is red.[(triple8 OR ((triple9) -> rule2) OR ((((triple10 triple6) -> rule1)) -> rule2))] Fiona is round.[(triple9 OR ((triple10 triple6) -> rule1))] Fiona is smart.[(triple10)] Fiona is young.[(triple11 OR ((triple10 triple7) -> rule6))] Gary is green.[(triple12)] Gary is red.[(triple13 OR ((triple14) -> rule2))] Gary is round.[(triple14)] Gary is smart.[(triple15)] @1: Dave is blue.[(((triple2) -> rule3) OR ((((triple4) -> rule4)) -> rule3))] Dave is young.[(((triple2) -> rule5) OR ((triple5 triple1) -> rule6) OR ((((triple4) -> rule4)) -> rule5))] Gary is young.[(((triple15 triple12) -> rule6))]
Dave is green.
("Dave" "is" "green" "+")
triple1
Dave is kind.
("Dave" "is" "kind" "+")
triple2
((triple4) -> (rule4 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
triple3
((triple4) -> (rule2 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
((((triple5 ((triple2) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Dave is round.
("Dave" "is" "round" "+")
triple4
((triple5 ((triple2) -> (rule3 % int2))) -> (rule1 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
triple5
Fiona is blue.
("Fiona" "is" "blue" "+")
triple6
Fiona is green.
("Fiona" "is" "green" "+")
triple7
Fiona is red.
("Fiona" "is" "red" "+")
triple8
((triple9) -> (rule2 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
((((triple10 triple6) -> (rule1 % int2))) -> (rule2 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
triple9
((triple10 triple6) -> (rule1 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
triple10
Fiona is young.
("Fiona" "is" "young" "+")
triple11
((triple10 triple7) -> (rule6 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
triple12
Gary is red.
("Gary" "is" "red" "+")
triple13
((triple14) -> (rule2 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
triple14
Gary is smart.
("Gary" "is" "smart" "+")
triple15
Dave is blue.
("Dave" "is" "blue" "+")
((triple2) -> (rule3 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
((((triple4) -> (rule4 % int2))) -> (rule3 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
((triple2) -> (rule5 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
((triple5 triple1) -> (rule6 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
((((triple4) -> (rule4 % int2))) -> (rule5 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
((triple15 triple12) -> (rule6 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1