Anne is green. Anne is nice. Dave is cold. Dave is green. Dave is nice. Dave is quiet. Dave is round. Gary is big. Gary is cold. Gary is nice. Harry is quiet. Harry is rough. If Gary is cold then Gary is green. All rough people are big. Round people are green. Nice people are round. Cold people are quiet. If someone is big and round then they are rough.
Anne is green.
("Anne" "is" "green" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is round.
("Dave" "is" "round" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is rough.
("Harry" "is" "rough" "+")
If Gary is cold then Gary is green.
((("Gary" "is" "cold" "+")) -> ("Gary" "is" "green" "+"))
All rough people are big.
((("someone" "is" "rough" "+")) -> ("someone" "is" "big" "+"))
Round people are green.
((("someone" "is" "round" "+")) -> ("someone" "is" "green" "+"))
Nice people are round.
((("someone" "is" "nice" "+")) -> ("someone" "is" "round" "+"))
Cold people are quiet.
((("someone" "is" "cold" "+")) -> ("someone" "is" "quiet" "+"))
If someone is big and round then they are rough.
((("someone" "is" "big" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "rough" "+"))
Harry is rough.
True
1
proof
[(triple12)]
("Harry" "is" "rough" "+")
triple12
Anne is not green.
False
1
inv-proof
[(triple1 OR ((((triple2) -> rule4)) -> rule3))]
("Anne" "is" "green" "-")
triple1
((((triple2) -> (rule4 % int2))) -> (rule3 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Gary is quiet.
True
2
proof
[(((triple9) -> rule5))]
("Gary" "is" "quiet" "+")
((triple9) -> (rule5 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is not quiet.
False
2
inv-proof
[(((triple9) -> rule5))]
("Gary" "is" "quiet" "-")
((triple9) -> (rule5 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Anne is not rough.
Unknown
inv-rconc
[@2: Anne is rough.[CWA. Example of deepest failure = (rule6 <- rule2 <- FAIL)]]
("Anne" "is" "rough" "-")
Anne is big.
Unknown
rconc
[@2: Anne is big.[CWA. Example of deepest failure = (rule2 <- rule6 <- FAIL)]]
("Anne" "is" "big" "+")
Anne is not cold.
Unknown
inv-random
[@0: Anne is cold.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "cold" "-")
Harry is nice.
Unknown
random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "+")
@0: Anne is green.[(triple1 OR ((((triple2) -> rule4)) -> rule3))] Anne is nice.[(triple2)] Dave is cold.[(triple3)] Dave is green.[(triple4 OR ((triple7) -> rule3) OR ((((triple5) -> rule4)) -> rule3))] Dave is nice.[(triple5)] Dave is quiet.[(triple6 OR ((triple3) -> rule5))] Dave is round.[(triple7 OR ((triple5) -> rule4))] Gary is big.[(triple8)] Gary is cold.[(triple9)] Gary is nice.[(triple10)] Harry is quiet.[(triple11)] Harry is rough.[(triple12)] @1: Anne is round.[(((triple2) -> rule4))] Gary is green.[(((triple9) -> rule1) OR ((((triple10) -> rule4)) -> rule3))] Gary is quiet.[(((triple9) -> rule5))] Gary is round.[(((triple10) -> rule4))] Harry is big.[(((triple12) -> rule2))] @2: Gary is rough.[(((triple8 ((triple10) -> rule4)) -> rule6))]
Anne is green.
("Anne" "is" "green" "+")
triple1
((((triple2) -> (rule4 % int2))) -> (rule3 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
triple2
Dave is cold.
("Dave" "is" "cold" "+")
triple3
Dave is green.
("Dave" "is" "green" "+")
triple4
((triple7) -> (rule3 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
((((triple5) -> (rule4 % int2))) -> (rule3 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
triple5
Dave is quiet.
("Dave" "is" "quiet" "+")
triple6
((triple3) -> (rule5 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
triple7
((triple5) -> (rule4 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
triple8
Gary is cold.
("Gary" "is" "cold" "+")
triple9
Gary is nice.
("Gary" "is" "nice" "+")
triple10
Harry is quiet.
("Harry" "is" "quiet" "+")
triple11
Harry is rough.
("Harry" "is" "rough" "+")
triple12
Anne is round.
("Anne" "is" "round" "+")
((triple2) -> (rule4 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
((triple9) -> (rule1 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
((((triple10) -> (rule4 % int2))) -> (rule3 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
((triple9) -> (rule5 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
((triple10) -> (rule4 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
((triple12) -> (rule2 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
((triple8 ((triple10) -> (rule4 % int2))) -> (rule6 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2