Anne is blue. Anne is red. Anne is rough. Anne is round. Anne is not white. Bob is not quiet. Bob is red. Bob is rough. Bob is round. Bob is white. Dave is not blue. Dave is not quiet. Dave is not red. Dave is rough. Harry is not cold. Harry is red. If Dave is red and Dave is cold then Dave is quiet. All red things are blue. If Dave is white then Dave is not red. If Anne is not round then Anne is rough. If something is blue then it is not quiet. If something is white and not round then it is not red.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is round.
("Anne" "is" "round" "+")
Anne is not white.
("Anne" "is" "white" "-")
Bob is not quiet.
("Bob" "is" "quiet" "-")
Bob is red.
("Bob" "is" "red" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is white.
("Bob" "is" "white" "+")
Dave is not blue.
("Dave" "is" "blue" "-")
Dave is not quiet.
("Dave" "is" "quiet" "-")
Dave is not red.
("Dave" "is" "red" "-")
Dave is rough.
("Dave" "is" "rough" "+")
Harry is not cold.
("Harry" "is" "cold" "-")
Harry is red.
("Harry" "is" "red" "+")
If Dave is red and Dave is cold then Dave is quiet.
((("Dave" "is" "red" "+") ("Dave" "is" "cold" "+")) -> ("Dave" "is" "quiet" "+"))
All red things are blue.
((("something" "is" "red" "+")) -> ("something" "is" "blue" "+"))
If Dave is white then Dave is not red.
((("Dave" "is" "white" "+")) -> ("Dave" "is" "red" "-"))
If Anne is not round then Anne is rough.
((("Anne" "is" "round" "~")) -> ("Anne" "is" "rough" "+"))
If something is blue then it is not quiet.
((("something" "is" "blue" "+")) -> ("something" "is" "quiet" "-"))
If something is white and not round then it is not red.
((("something" "is" "white" "+") ("something" "is" "round" "~")) -> ("something" "is" "red" "-"))
Bob is not quiet.
True
1
proof
[(triple6 OR ((((triple7) -> rule2)) -> rule5))]
("Bob" "is" "quiet" "-")
triple6
((((triple7) -> (rule2 % int2))) -> (rule5 % int1))
Bob is not quiet.
("Bob" "is" "quiet" "-")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is not rough.
False
1
inv-proof
[(triple8)]
("Bob" "is" "rough" "-")
triple8
Anne is not quiet.
True
2
proof
[(((triple1) -> rule5) OR ((((triple2) -> rule2)) -> rule5))]
("Anne" "is" "quiet" "-")
((triple1) -> (rule5 % int1))
Anne is not quiet.
("Anne" "is" "quiet" "-")
int1
((((triple2) -> (rule2 % int2))) -> (rule5 % int1))
Anne is not quiet.
("Anne" "is" "quiet" "-")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Bob is not blue.
False
2
inv-proof
[(((triple7) -> rule2))]
("Bob" "is" "blue" "-")
((triple7) -> (rule2 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Harry is not quiet.
True
3
proof
[(((((triple16) -> rule2)) -> rule5))]
("Harry" "is" "quiet" "-")
((((triple16) -> (rule2 % int2))) -> (rule5 % int1))
Harry is not quiet.
("Harry" "is" "quiet" "-")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is quiet.
False
3
inv-proof
[(((((triple16) -> rule2)) -> rule5))]
("Harry" "is" "quiet" "+")
((((triple16) -> (rule2 % int2))) -> (rule5 % int1))
Harry is not quiet.
("Harry" "is" "quiet" "-")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Bob is not cold.
Unknown
inv-random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "-")
Harry is round.
Unknown
random
[@0: Harry is round.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "round" "+")
Dave is not white.
Unknown
inv-random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "-")
Harry is white.
Unknown
random
[@0: Harry is white.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "white" "+")
Anne is not cold.
Unknown
inv-random
[@0: Anne is cold.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "cold" "-")
Dave is cold.
Unknown
random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "+")
@0: Anne is blue.[(triple1 OR ((triple2) -> rule2))] Anne is not white.[(triple5)] Anne is red.[(triple2)] Anne is rough.[(triple3)] Anne is round.[(triple4)] Bob is not quiet.[(triple6 OR ((((triple7) -> rule2)) -> rule5))] Bob is red.[(triple7)] Bob is rough.[(triple8)] Bob is round.[(triple9)] Bob is white.[(triple10)] Dave is not blue.[(triple11)] Dave is not quiet.[(triple12)] Dave is not red.[(triple13)] Dave is rough.[(triple14)] Harry is not cold.[(triple15)] Harry is red.[(triple16)] @1: Anne is not quiet.[(((triple1) -> rule5) OR ((((triple2) -> rule2)) -> rule5))] Bob is blue.[(((triple7) -> rule2))] Harry is blue.[(((triple16) -> rule2))] @2: Harry is not quiet.[(((((triple16) -> rule2)) -> rule5))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
((triple2) -> (rule2 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is not white.
("Anne" "is" "white" "-")
triple5
Anne is red.
("Anne" "is" "red" "+")
triple2
Anne is rough.
("Anne" "is" "rough" "+")
triple3
Anne is round.
("Anne" "is" "round" "+")
triple4
Bob is not quiet.
("Bob" "is" "quiet" "-")
triple6
((((triple7) -> (rule2 % int2))) -> (rule5 % int1))
Bob is not quiet.
("Bob" "is" "quiet" "-")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
triple7
Bob is rough.
("Bob" "is" "rough" "+")
triple8
Bob is round.
("Bob" "is" "round" "+")
triple9
Bob is white.
("Bob" "is" "white" "+")
triple10
Dave is not blue.
("Dave" "is" "blue" "-")
triple11
Dave is not quiet.
("Dave" "is" "quiet" "-")
triple12
Dave is not red.
("Dave" "is" "red" "-")
triple13
Dave is rough.
("Dave" "is" "rough" "+")
triple14
Harry is not cold.
("Harry" "is" "cold" "-")
triple15
Harry is red.
("Harry" "is" "red" "+")
triple16
Anne is not quiet.
("Anne" "is" "quiet" "-")
((triple1) -> (rule5 % int1))
Anne is not quiet.
("Anne" "is" "quiet" "-")
int1
((((triple2) -> (rule2 % int2))) -> (rule5 % int1))
Anne is not quiet.
("Anne" "is" "quiet" "-")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
((triple7) -> (rule2 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
((triple16) -> (rule2 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is not quiet.
("Harry" "is" "quiet" "-")
((((triple16) -> (rule2 % int2))) -> (rule5 % int1))
Harry is not quiet.
("Harry" "is" "quiet" "-")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2