Anne is big. Anne is cold. Anne is not green. Anne is not nice. Anne is round. Bob is big. Bob is cold. Bob is nice. Bob is quiet. Bob is round. Gary is big. Gary is cold. Gary is quiet. Harry is furry. Harry is round. All round people are quiet. All quiet people are furry. If someone is cold and not quiet then they are furry.
Anne is big.
("Anne" "is" "big" "+")
Anne is cold.
("Anne" "is" "cold" "+")
Anne is not green.
("Anne" "is" "green" "-")
Anne is not nice.
("Anne" "is" "nice" "-")
Anne is round.
("Anne" "is" "round" "+")
Bob is big.
("Bob" "is" "big" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is round.
("Bob" "is" "round" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is round.
("Harry" "is" "round" "+")
All round people are quiet.
((("someone" "is" "round" "+")) -> ("someone" "is" "quiet" "+"))
All quiet people are furry.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "furry" "+"))
If someone is cold and not quiet then they are furry.
((("someone" "is" "cold" "+") ("someone" "is" "quiet" "~")) -> ("someone" "is" "furry" "+"))
Harry is round.
True
1
proof
[(triple15)]
("Harry" "is" "round" "+")
triple15
Anne is green.
False
1
inv-proof
[(triple3)]
("Anne" "is" "green" "+")
triple3
Anne is quiet.
True
2
proof
[(((triple5) -> rule1))]
("Anne" "is" "quiet" "+")
((triple5) -> (rule1 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Bob is not furry.
False
2
inv-proof
[(((triple9) -> rule2) OR ((((triple10) -> rule1)) -> rule2))]
("Bob" "is" "furry" "-")
((triple9) -> (rule2 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
((((triple10) -> (rule1 % int2))) -> (rule2 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Anne is furry.
True
3
proof
[(((((triple5) -> rule1)) -> rule2))]
("Anne" "is" "furry" "+")
((((triple5) -> (rule1 % int2))) -> (rule2 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is not furry.
False
3
inv-proof
[(((((triple5) -> rule1)) -> rule2))]
("Anne" "is" "furry" "-")
((((triple5) -> (rule1 % int2))) -> (rule2 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Gary is not green.
Unknown
inv-random
[@0: Gary is green.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "green" "-")
Bob is green.
Unknown
random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "+")
Harry is not cold.
Unknown
inv-random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "-")
Gary is nice.
Unknown
random
[@0: Gary is nice.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "nice" "+")
Harry is not big.
Unknown
inv-random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "-")
Harry is nice.
Unknown
random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "+")
@0: Anne is big.[(triple1)] Anne is cold.[(triple2)] Anne is not green.[(triple3)] Anne is not nice.[(triple4)] Anne is round.[(triple5)] Bob is big.[(triple6)] Bob is cold.[(triple7)] Bob is nice.[(triple8)] Bob is quiet.[(triple9 OR ((triple10) -> rule1))] Bob is round.[(triple10)] Gary is big.[(triple11)] Gary is cold.[(triple12)] Gary is quiet.[(triple13)] Harry is furry.[(triple14 OR ((((triple15) -> rule1)) -> rule2))] Harry is round.[(triple15)] @1: Anne is quiet.[(((triple5) -> rule1))] Bob is furry.[(((triple9) -> rule2) OR ((((triple10) -> rule1)) -> rule2))] Gary is furry.[(((triple13) -> rule2))] Harry is quiet.[(((triple15) -> rule1))] @2: Anne is furry.[(((((triple5) -> rule1)) -> rule2))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is cold.
("Anne" "is" "cold" "+")
triple2
Anne is not green.
("Anne" "is" "green" "-")
triple3
Anne is not nice.
("Anne" "is" "nice" "-")
triple4
Anne is round.
("Anne" "is" "round" "+")
triple5
Bob is big.
("Bob" "is" "big" "+")
triple6
Bob is cold.
("Bob" "is" "cold" "+")
triple7
Bob is nice.
("Bob" "is" "nice" "+")
triple8
Bob is quiet.
("Bob" "is" "quiet" "+")
triple9
((triple10) -> (rule1 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
triple10
Gary is big.
("Gary" "is" "big" "+")
triple11
Gary is cold.
("Gary" "is" "cold" "+")
triple12
Gary is quiet.
("Gary" "is" "quiet" "+")
triple13
Harry is furry.
("Harry" "is" "furry" "+")
triple14
((((triple15) -> (rule1 % int2))) -> (rule2 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
triple15
Anne is quiet.
("Anne" "is" "quiet" "+")
((triple5) -> (rule1 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
((triple9) -> (rule2 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
((((triple10) -> (rule1 % int2))) -> (rule2 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
((triple13) -> (rule2 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple15) -> (rule1 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
((((triple5) -> (rule1 % int2))) -> (rule2 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2