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