Anne is cold. Anne is green. Anne is not white. Anne is young. Bob is nice. Bob is quiet. Charlie is blue. Charlie is white. Gary is blue. Gary is not cold. Gary is not green. Gary is nice. Gary is quiet. Gary is white. Gary is young. If someone is cold then they are nice. All nice, green people are not quiet. If Charlie is green then Charlie is nice. If Anne is quiet and Anne is not blue then Anne is cold. If someone is cold then they are young. If Anne is cold and Anne is young then Anne is green.
Anne is cold.
("Anne" "is" "cold" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is not white.
("Anne" "is" "white" "-")
Anne is young.
("Anne" "is" "young" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is not cold.
("Gary" "is" "cold" "-")
Gary is not green.
("Gary" "is" "green" "-")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is white.
("Gary" "is" "white" "+")
Gary is young.
("Gary" "is" "young" "+")
If someone is cold then they are nice.
((("someone" "is" "cold" "+")) -> ("someone" "is" "nice" "+"))
All nice, green people are not quiet.
((("someone" "is" "nice" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "quiet" "-"))
If Charlie is green then Charlie is nice.
((("Charlie" "is" "green" "+")) -> ("Charlie" "is" "nice" "+"))
If Anne is quiet and Anne is not blue then Anne is cold.
((("Anne" "is" "quiet" "+") ("Anne" "is" "blue" "~")) -> ("Anne" "is" "cold" "+"))
If someone is cold then they are young.
((("someone" "is" "cold" "+")) -> ("someone" "is" "young" "+"))
If Anne is cold and Anne is young then Anne is green.
((("Anne" "is" "cold" "+") ("Anne" "is" "young" "+")) -> ("Anne" "is" "green" "+"))
Gary is quiet.
True
1
proof
[(triple13)]
("Gary" "is" "quiet" "+")
triple13
Gary is cold.
False
1
inv-proof
[(triple10)]
("Gary" "is" "cold" "+")
triple10
Anne is nice.
True
2
proof
[(((triple1) -> rule1))]
("Anne" "is" "nice" "+")
((triple1) -> (rule1 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is not nice.
False
2
inv-proof
[(((triple1) -> rule1))]
("Anne" "is" "nice" "-")
((triple1) -> (rule1 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is not quiet.
True
4
proof
[(((((triple1) -> rule1) triple2) -> rule2) OR ((((triple1) -> rule1) ((triple1 triple4) -> rule6)) -> rule2) OR ((((triple1) -> rule1) ((triple1 ((triple1) -> rule5)) -> rule6)) -> rule2))]
("Anne" "is" "quiet" "-")
((((triple1) -> (rule1 % int2)) triple2) -> (rule2 % int1))
Anne is not quiet.
("Anne" "is" "quiet" "-")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
((((triple1) -> (rule1 % int3)) ((triple1 triple4) -> (rule6 % int2))) -> (rule2 % int1))
Anne is not quiet.
("Anne" "is" "quiet" "-")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
((((triple1) -> (rule1 % int4)) ((triple1 ((triple1) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Anne is not quiet.
("Anne" "is" "quiet" "-")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is nice.
("Anne" "is" "nice" "+")
int4
Anne is quiet.
False
4
inv-proof
[(((((triple1) -> rule1) triple2) -> rule2) OR ((((triple1) -> rule1) ((triple1 triple4) -> rule6)) -> rule2) OR ((((triple1) -> rule1) ((triple1 ((triple1) -> rule5)) -> rule6)) -> rule2))]
("Anne" "is" "quiet" "+")
((((triple1) -> (rule1 % int2)) triple2) -> (rule2 % int1))
Anne is not quiet.
("Anne" "is" "quiet" "-")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
((((triple1) -> (rule1 % int3)) ((triple1 triple4) -> (rule6 % int2))) -> (rule2 % int1))
Anne is not quiet.
("Anne" "is" "quiet" "-")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
((((triple1) -> (rule1 % int4)) ((triple1 ((triple1) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Anne is not quiet.
("Anne" "is" "quiet" "-")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is nice.
("Anne" "is" "nice" "+")
int4
Charlie is not nice.
Unknown
inv-rconc
[@1: Charlie is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "nice" "-")
Bob is young.
Unknown
rconc
[@1: Bob is young.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Bob" "is" "young" "+")
Charlie is not young.
Unknown
inv-rconc
[@1: Charlie is young.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Charlie" "is" "young" "-")
Charlie is quiet.
Unknown
random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "+")
Bob is not green.
Unknown
inv-random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "-")
Anne is blue.
Unknown
random
[@0: Anne is blue.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "blue" "+")
@0: Anne is cold.[(triple1)] Anne is green.[(triple2 OR ((triple1 triple4) -> rule6) OR ((triple1 ((triple1) -> rule5)) -> rule6))] Anne is not white.[(triple3)] Anne is young.[(triple4 OR ((triple1) -> rule5))] Bob is nice.[(triple5)] Bob is quiet.[(triple6)] Charlie is blue.[(triple7)] Charlie is white.[(triple8)] Gary is blue.[(triple9)] Gary is nice.[(triple12)] Gary is not cold.[(triple10)] Gary is not green.[(triple11)] Gary is quiet.[(triple13)] Gary is white.[(triple14)] Gary is young.[(triple15)] @1: Anne is nice.[(((triple1) -> rule1))] @2: Anne is not quiet.[(((((triple1) -> rule1) triple2) -> rule2) OR ((((triple1) -> rule1) ((triple1 triple4) -> rule6)) -> rule2) OR ((((triple1) -> rule1) ((triple1 ((triple1) -> rule5)) -> rule6)) -> rule2))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Anne is green.
("Anne" "is" "green" "+")
triple2
((triple1 triple4) -> (rule6 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
((triple1 ((triple1) -> (rule5 % int2))) -> (rule6 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is not white.
("Anne" "is" "white" "-")
triple3
Anne is young.
("Anne" "is" "young" "+")
triple4
((triple1) -> (rule5 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
triple5
Bob is quiet.
("Bob" "is" "quiet" "+")
triple6
Charlie is blue.
("Charlie" "is" "blue" "+")
triple7
Charlie is white.
("Charlie" "is" "white" "+")
triple8
Gary is blue.
("Gary" "is" "blue" "+")
triple9
Gary is nice.
("Gary" "is" "nice" "+")
triple12
Gary is not cold.
("Gary" "is" "cold" "-")
triple10
Gary is not green.
("Gary" "is" "green" "-")
triple11
Gary is quiet.
("Gary" "is" "quiet" "+")
triple13
Gary is white.
("Gary" "is" "white" "+")
triple14
Gary is young.
("Gary" "is" "young" "+")
triple15
Anne is nice.
("Anne" "is" "nice" "+")
((triple1) -> (rule1 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is not quiet.
("Anne" "is" "quiet" "-")
((((triple1) -> (rule1 % int2)) triple2) -> (rule2 % int1))
Anne is not quiet.
("Anne" "is" "quiet" "-")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
((((triple1) -> (rule1 % int3)) ((triple1 triple4) -> (rule6 % int2))) -> (rule2 % int1))
Anne is not quiet.
("Anne" "is" "quiet" "-")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
((((triple1) -> (rule1 % int4)) ((triple1 ((triple1) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Anne is not quiet.
("Anne" "is" "quiet" "-")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is nice.
("Anne" "is" "nice" "+")
int4