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