Anne is cold. Anne is not rough. Bob is nice. Charlie is white. Charlie is young. Harry is not white. Harry is young. All nice people are cold. Rough people are nice. If Harry is young and Harry is not white then Harry is rough. If someone is cold and not young then they are not green. Green people are furry. Young, white people are furry. If Anne is nice and Anne is green then Anne is cold. If Harry is rough and Harry is cold then Harry is green.
Anne is cold.
("Anne" "is" "cold" "+")
Anne is not rough.
("Anne" "is" "rough" "-")
Bob is nice.
("Bob" "is" "nice" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Harry is not white.
("Harry" "is" "white" "-")
Harry is young.
("Harry" "is" "young" "+")
All nice people are cold.
((("someone" "is" "nice" "+")) -> ("someone" "is" "cold" "+"))
Rough people are nice.
((("someone" "is" "rough" "+")) -> ("someone" "is" "nice" "+"))
If Harry is young and Harry is not white then Harry is rough.
((("Harry" "is" "young" "+") ("Harry" "is" "white" "~")) -> ("Harry" "is" "rough" "+"))
If someone is cold and not young then they are not green.
((("someone" "is" "cold" "+") ("someone" "is" "young" "~")) -> ("someone" "is" "green" "-"))
Green people are furry.
((("someone" "is" "green" "+")) -> ("someone" "is" "furry" "+"))
Young, white people are furry.
((("someone" "is" "young" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "furry" "+"))
If Anne is nice and Anne is green then Anne is cold.
((("Anne" "is" "nice" "+") ("Anne" "is" "green" "+")) -> ("Anne" "is" "cold" "+"))
If Harry is rough and Harry is cold then Harry is green.
((("Harry" "is" "rough" "+") ("Harry" "is" "cold" "+")) -> ("Harry" "is" "green" "+"))
Anne is cold.
True
1
proof
[(triple1)]
("Anne" "is" "cold" "+")
triple1
Bob is not nice.
False
1
inv-proof
[(triple3)]
("Bob" "is" "nice" "-")
triple3
Charlie is furry.
True
3
proof
[(((triple5 triple4) -> rule6))]
("Charlie" "is" "furry" "+")
((triple5 triple4) -> (rule6 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is not furry.
False
3
inv-proof
[(((triple5 triple4) -> rule6))]
("Charlie" "is" "furry" "-")
((triple5 triple4) -> (rule6 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Harry is nice.
True
4
proof
[(((((triple7 triple6) -> rule3)) -> rule2))]
("Harry" "is" "nice" "+")
((((triple7 triple6) -> (rule3 % int2))) -> (rule2 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is not nice.
False
4
inv-proof
[(((((triple7 triple6) -> rule3)) -> rule2))]
("Harry" "is" "nice" "-")
((((triple7 triple6) -> (rule3 % int2))) -> (rule2 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is cold.
True
5
proof
[(((((((triple7 triple6) -> rule3)) -> rule2)) -> rule1))]
("Harry" "is" "cold" "+")
((((((triple7 triple6) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Harry is not cold.
False
5
inv-proof
[(((((((triple7 triple6) -> rule3)) -> rule2)) -> rule1))]
("Harry" "is" "cold" "-")
((((((triple7 triple6) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Harry is green.
True
9
proof
[(((((triple7 triple6) -> rule3) ((((((triple7 triple6) -> rule3)) -> rule2)) -> rule1)) -> rule8))]
("Harry" "is" "green" "+")
((((triple7 triple6) -> (rule3 % int4)) ((((((triple7 triple6) -> (rule3 % int4))) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is rough.
("Harry" "is" "rough" "+")
int4
Harry is not green.
False
9
inv-proof
[(((((triple7 triple6) -> rule3) ((((((triple7 triple6) -> rule3)) -> rule2)) -> rule1)) -> rule8))]
("Harry" "is" "green" "-")
((((triple7 triple6) -> (rule3 % int4)) ((((((triple7 triple6) -> (rule3 % int4))) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is rough.
("Harry" "is" "rough" "+")
int4
Harry is furry.
True
10
proof
[(((((((triple7 triple6) -> rule3) ((((((triple7 triple6) -> rule3)) -> rule2)) -> rule1)) -> rule8)) -> rule5))]
("Harry" "is" "furry" "+")
((((((triple7 triple6) -> (rule3 % int5)) ((((((triple7 triple6) -> (rule3 % int5))) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Harry is nice.
("Harry" "is" "nice" "+")
int4
Harry is rough.
("Harry" "is" "rough" "+")
int5
Harry is not furry.
False
10
inv-proof
[(((((((triple7 triple6) -> rule3) ((((((triple7 triple6) -> rule3)) -> rule2)) -> rule1)) -> rule8)) -> rule5))]
("Harry" "is" "furry" "-")
((((((triple7 triple6) -> (rule3 % int5)) ((((((triple7 triple6) -> (rule3 % int5))) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Harry is nice.
("Harry" "is" "nice" "+")
int4
Harry is rough.
("Harry" "is" "rough" "+")
int5
Bob is not furry.
Unknown
inv-rconc
[@1: Bob is furry.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Bob" "is" "furry" "-")
Anne is nice.
Unknown
rconc
[@1: Anne is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "nice" "+")
Charlie is not cold.
Unknown
inv-rconc
[@2: Charlie is cold.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Charlie" "is" "cold" "-")
Charlie is nice.
Unknown
rconc
[@1: Charlie is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "nice" "+")
Anne is not furry.
Unknown
inv-rconc
[@1: Anne is furry.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Anne" "is" "furry" "-")
Charlie is green.
Unknown
random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "+")
Bob is not rough.
Unknown
inv-random
[@0: Bob is rough.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "rough" "-")
Charlie is rough.
Unknown
random
[@0: Charlie is rough.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "rough" "+")
Anne is not young.
Unknown
inv-random
[@0: Anne is young.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "young" "-")
Bob is young.
Unknown
random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "+")
Bob is not white.
Unknown
inv-random
[@0: Bob is white.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "white" "-")
Anne is white.
Unknown
random
[@0: Anne is white.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "white" "+")
@0: Anne is cold.[(triple1)] Anne is not rough.[(triple2)] Bob is nice.[(triple3)] Charlie is white.[(triple4)] Charlie is young.[(triple5)] Harry is not white.[(triple6)] Harry is young.[(triple7)] @1: Bob is cold.[(((triple3) -> rule1))] Charlie is furry.[(((triple5 triple4) -> rule6))] Harry is rough.[(((triple7 triple6) -> rule3))] @2: Harry is nice.[(((((triple7 triple6) -> rule3)) -> rule2))] @3: Harry is cold.[(((((((triple7 triple6) -> rule3)) -> rule2)) -> rule1))] @4: Harry is green.[(((((triple7 triple6) -> rule3) ((((((triple7 triple6) -> rule3)) -> rule2)) -> rule1)) -> rule8))] @5: Harry is furry.[(((((((triple7 triple6) -> rule3) ((((((triple7 triple6) -> rule3)) -> rule2)) -> rule1)) -> rule8)) -> rule5))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Anne is not rough.
("Anne" "is" "rough" "-")
triple2
Bob is nice.
("Bob" "is" "nice" "+")
triple3
Charlie is white.
("Charlie" "is" "white" "+")
triple4
Charlie is young.
("Charlie" "is" "young" "+")
triple5
Harry is not white.
("Harry" "is" "white" "-")
triple6
Harry is young.
("Harry" "is" "young" "+")
triple7
Bob is cold.
("Bob" "is" "cold" "+")
((triple3) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
((triple5 triple4) -> (rule6 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
((triple7 triple6) -> (rule3 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
((((triple7 triple6) -> (rule3 % int2))) -> (rule2 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
((((((triple7 triple6) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Harry is green.
("Harry" "is" "green" "+")
((((triple7 triple6) -> (rule3 % int4)) ((((((triple7 triple6) -> (rule3 % int4))) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is rough.
("Harry" "is" "rough" "+")
int4
Harry is furry.
("Harry" "is" "furry" "+")
((((((triple7 triple6) -> (rule3 % int5)) ((((((triple7 triple6) -> (rule3 % int5))) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Harry is nice.
("Harry" "is" "nice" "+")
int4
Harry is rough.
("Harry" "is" "rough" "+")
int5