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