Anne is cold. Anne is quiet. Anne is not round. Dave is blue. Dave is quiet. Dave is red. Dave is round. Dave is smart. Fiona is cold. Fiona is round. Fiona is smart. Fiona is young. If someone is round and smart then they are quiet. If someone is young then they are round. If Anne is smart and Anne is cold then Anne is not blue.
Anne is cold.
("Anne" "is" "cold" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is not round.
("Anne" "is" "round" "-")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Fiona is young.
("Fiona" "is" "young" "+")
If someone is round and smart then they are quiet.
((("someone" "is" "round" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "quiet" "+"))
If someone is young then they are round.
((("someone" "is" "young" "+")) -> ("someone" "is" "round" "+"))
If Anne is smart and Anne is cold then Anne is not blue.
((("Anne" "is" "smart" "+") ("Anne" "is" "cold" "+")) -> ("Anne" "is" "blue" "-"))
Fiona is smart.
True
1
proof
[(triple11)]
("Fiona" "is" "smart" "+")
triple11
Dave is not round.
False
1
inv-proof
[(triple7)]
("Dave" "is" "round" "-")
triple7
Dave is not young.
Unknown
inv-random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "-")
Fiona is red.
Unknown
random
[@0: Fiona is red.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "red" "+")
@0: Anne is cold.[(triple1)] Anne is not round.[(triple3)] Anne is quiet.[(triple2)] Dave is blue.[(triple4)] Dave is quiet.[(triple5 OR ((triple7 triple8) -> rule1))] Dave is red.[(triple6)] Dave is round.[(triple7)] Dave is smart.[(triple8)] Fiona is cold.[(triple9)] Fiona is round.[(triple10 OR ((triple12) -> rule2))] Fiona is smart.[(triple11)] Fiona is young.[(triple12)] @1: Fiona is quiet.[(((triple10 triple11) -> rule1) OR ((((triple12) -> rule2) triple11) -> rule1))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Anne is not round.
("Anne" "is" "round" "-")
triple3
Anne is quiet.
("Anne" "is" "quiet" "+")
triple2
Dave is blue.
("Dave" "is" "blue" "+")
triple4
Dave is quiet.
("Dave" "is" "quiet" "+")
triple5
((triple7 triple8) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
triple6
Dave is round.
("Dave" "is" "round" "+")
triple7
Dave is smart.
("Dave" "is" "smart" "+")
triple8
Fiona is cold.
("Fiona" "is" "cold" "+")
triple9
Fiona is round.
("Fiona" "is" "round" "+")
triple10
((triple12) -> (rule2 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
triple11
Fiona is young.
("Fiona" "is" "young" "+")
triple12
Fiona is quiet.
("Fiona" "is" "quiet" "+")
((triple10 triple11) -> (rule1 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
((((triple12) -> (rule2 % int2)) triple11) -> (rule1 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2