Anne is quiet. Anne is young. Dave is quiet. Gary is cold. Gary is green. Harry is cold. Harry is green. Harry is nice. Harry is quiet. Harry is red. Harry is not smart. Harry is not young. If something is red then it is cold. If Anne is cold then Anne is not nice. All green things are quiet. If something is green and red then it is nice. If something is quiet and cold then it is red. If Harry is nice then Harry is quiet.
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is young.
("Anne" "is" "young" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is green.
("Gary" "is" "green" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is not smart.
("Harry" "is" "smart" "-")
Harry is not young.
("Harry" "is" "young" "-")
If something is red then it is cold.
((("something" "is" "red" "+")) -> ("something" "is" "cold" "+"))
If Anne is cold then Anne is not nice.
((("Anne" "is" "cold" "+")) -> ("Anne" "is" "nice" "-"))
All green things are quiet.
((("something" "is" "green" "+")) -> ("something" "is" "quiet" "+"))
If something is green and red then it is nice.
((("something" "is" "green" "+") ("something" "is" "red" "+")) -> ("something" "is" "nice" "+"))
If something is quiet and cold then it is red.
((("something" "is" "quiet" "+") ("something" "is" "cold" "+")) -> ("something" "is" "red" "+"))
If Harry is nice then Harry is quiet.
((("Harry" "is" "nice" "+")) -> ("Harry" "is" "quiet" "+"))
Harry is green.
True
1
proof
[(triple7)]
("Harry" "is" "green" "+")
triple7
Harry is not red.
False
1
inv-proof
[(triple10 OR ((triple9 triple6) -> rule5) OR ((((triple7) -> rule3) triple6) -> rule5) OR ((((triple8) -> rule6) triple6) -> rule5))]
("Harry" "is" "red" "-")
triple10
((triple9 triple6) -> (rule5 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
((((triple7) -> (rule3 % int2)) triple6) -> (rule5 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
((((triple8) -> (rule6 % int2)) triple6) -> (rule5 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Gary is quiet.
True
2
proof
[(((triple5) -> rule3))]
("Gary" "is" "quiet" "+")
((triple5) -> (rule3 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is not quiet.
False
2
inv-proof
[(((triple5) -> rule3))]
("Gary" "is" "quiet" "-")
((triple5) -> (rule3 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is red.
True
4
proof
[(((((triple5) -> rule3) triple4) -> rule5))]
("Gary" "is" "red" "+")
((((triple5) -> (rule3 % int2)) triple4) -> (rule5 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is not red.
False
4
inv-proof
[(((((triple5) -> rule3) triple4) -> rule5))]
("Gary" "is" "red" "-")
((((triple5) -> (rule3 % int2)) triple4) -> (rule5 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is nice.
True
6
proof
[(((triple5 ((((triple5) -> rule3) triple4) -> rule5)) -> rule4))]
("Gary" "is" "nice" "+")
((triple5 ((((triple5) -> (rule3 % int3)) triple4) -> (rule5 % int2))) -> (rule4 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Gary is not nice.
False
6
inv-proof
[(((triple5 ((((triple5) -> rule3) triple4) -> rule5)) -> rule4))]
("Gary" "is" "nice" "-")
((triple5 ((((triple5) -> (rule3 % int3)) triple4) -> (rule5 % int2))) -> (rule4 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Dave is not red.
Unknown
inv-rconc
[@2: Dave is red.[CWA. Example of deepest failure = (rule5 <- rule1 <- FAIL)]]
("Dave" "is" "red" "-")
Anne is cold.
Unknown
rconc
[@2: Anne is cold.[CWA. Example of deepest failure = (rule1 <- rule5 <- FAIL)]]
("Anne" "is" "cold" "+")
Anne is not nice.
Unknown
inv-rconc
[@1: Anne is nice.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Anne" "is" "nice" "-")
Dave is cold.
Unknown
rconc
[@2: Dave is cold.[CWA. Example of deepest failure = (rule1 <- rule5 <- FAIL)]]
("Dave" "is" "cold" "+")
Dave is not young.
Unknown
inv-random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "-")
Dave is smart.
Unknown
random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "+")
Anne is not green.
Unknown
inv-random
[@0: Anne is green.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "green" "-")
Gary is smart.
Unknown
random
[@0: Gary is smart.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "smart" "+")
@0: Anne is quiet.[(triple1)] Anne is young.[(triple2)] Dave is quiet.[(triple3)] Gary is cold.[(triple4)] Gary is green.[(triple5)] Harry is cold.[(triple6 OR ((triple10) -> rule1))] Harry is green.[(triple7)] Harry is nice.[(triple8 OR ((triple7 triple10) -> rule4) OR ((triple7 ((triple9 triple6) -> rule5)) -> rule4) OR ((triple7 ((((triple7) -> rule3) triple6) -> rule5)) -> rule4))] Harry is not smart.[(triple11)] Harry is not young.[(triple12)] Harry is quiet.[(triple9 OR ((triple7) -> rule3) OR ((triple8) -> rule6) OR ((((triple7 triple10) -> rule4)) -> rule6))] Harry is red.[(triple10 OR ((triple9 triple6) -> rule5) OR ((((triple7) -> rule3) triple6) -> rule5) OR ((((triple8) -> rule6) triple6) -> rule5))] @1: Gary is quiet.[(((triple5) -> rule3))] @2: Gary is red.[(((((triple5) -> rule3) triple4) -> rule5))] @3: Gary is nice.[(((triple5 ((((triple5) -> rule3) triple4) -> rule5)) -> rule4))]
Anne is quiet.
("Anne" "is" "quiet" "+")
triple1
Anne is young.
("Anne" "is" "young" "+")
triple2
Dave is quiet.
("Dave" "is" "quiet" "+")
triple3
Gary is cold.
("Gary" "is" "cold" "+")
triple4
Gary is green.
("Gary" "is" "green" "+")
triple5
Harry is cold.
("Harry" "is" "cold" "+")
triple6
((triple10) -> (rule1 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
triple7
Harry is nice.
("Harry" "is" "nice" "+")
triple8
((triple7 triple10) -> (rule4 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
((triple7 ((triple9 triple6) -> (rule5 % int2))) -> (rule4 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
((triple7 ((((triple7) -> (rule3 % int3)) triple6) -> (rule5 % int2))) -> (rule4 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Harry is not smart.
("Harry" "is" "smart" "-")
triple11
Harry is not young.
("Harry" "is" "young" "-")
triple12
Harry is quiet.
("Harry" "is" "quiet" "+")
triple9
((triple7) -> (rule3 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
((triple8) -> (rule6 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
((((triple7 triple10) -> (rule4 % int2))) -> (rule6 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
triple10
((triple9 triple6) -> (rule5 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
((((triple7) -> (rule3 % int2)) triple6) -> (rule5 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
((((triple8) -> (rule6 % int2)) triple6) -> (rule5 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
((triple5) -> (rule3 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
((((triple5) -> (rule3 % int2)) triple4) -> (rule5 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
((triple5 ((((triple5) -> (rule3 % int3)) triple4) -> (rule5 % int2))) -> (rule4 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3