Anne is not cold. Anne is nice. Anne is red. Bob is nice. Bob is not red. Dave is kind. Harry is not green. Harry is not kind. Harry is red. Harry is rough. Harry is young. If something is red and kind then it is young. Red, green things are young. If something is rough then it is not kind. Green things are cold. If something is cold and red then it is nice. If Dave is young then Dave is green. Kind things are red. If Bob is red and Bob is young then Bob is green.
Anne is not cold.
("Anne" "is" "cold" "-")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is red.
("Anne" "is" "red" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is not red.
("Bob" "is" "red" "-")
Dave is kind.
("Dave" "is" "kind" "+")
Harry is not green.
("Harry" "is" "green" "-")
Harry is not kind.
("Harry" "is" "kind" "-")
Harry is red.
("Harry" "is" "red" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is young.
("Harry" "is" "young" "+")
If something is red and kind then it is young.
((("something" "is" "red" "+") ("something" "is" "kind" "+")) -> ("something" "is" "young" "+"))
Red, green things are young.
((("something" "is" "red" "+") ("something" "is" "green" "+")) -> ("something" "is" "young" "+"))
If something is rough then it is not kind.
((("something" "is" "rough" "+")) -> ("something" "is" "kind" "-"))
Green things are cold.
((("something" "is" "green" "+")) -> ("something" "is" "cold" "+"))
If something is cold and red then it is nice.
((("something" "is" "cold" "+") ("something" "is" "red" "+")) -> ("something" "is" "nice" "+"))
If Dave is young then Dave is green.
((("Dave" "is" "young" "+")) -> ("Dave" "is" "green" "+"))
Kind things are red.
((("something" "is" "kind" "+")) -> ("something" "is" "red" "+"))
If Bob is red and Bob is young then Bob is green.
((("Bob" "is" "red" "+") ("Bob" "is" "young" "+")) -> ("Bob" "is" "green" "+"))
Anne is red.
True
1
proof
[(triple3)]
("Anne" "is" "red" "+")
triple3
Anne is cold.
False
1
inv-proof
[(triple1)]
("Anne" "is" "cold" "+")
triple1
Dave is red.
True
2
proof
[(((triple6) -> rule7))]
("Dave" "is" "red" "+")
((triple6) -> (rule7 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is not red.
False
2
inv-proof
[(((triple6) -> rule7))]
("Dave" "is" "red" "-")
((triple6) -> (rule7 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is young.
True
4
proof
[(((((triple6) -> rule7) triple6) -> rule1))]
("Dave" "is" "young" "+")
((((triple6) -> (rule7 % int2)) triple6) -> (rule1 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is not young.
False
4
inv-proof
[(((((triple6) -> rule7) triple6) -> rule1))]
("Dave" "is" "young" "-")
((((triple6) -> (rule7 % int2)) triple6) -> (rule1 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is green.
True
5
proof
[(((((((triple6) -> rule7) triple6) -> rule1)) -> rule6))]
("Dave" "is" "green" "+")
((((((triple6) -> (rule7 % int3)) triple6) -> (rule1 % int2))) -> (rule6 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
Dave is not green.
False
5
inv-proof
[(((((((triple6) -> rule7) triple6) -> rule1)) -> rule6))]
("Dave" "is" "green" "-")
((((((triple6) -> (rule7 % int3)) triple6) -> (rule1 % int2))) -> (rule6 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
Dave is cold.
True
6
proof
[(((((((((triple6) -> rule7) triple6) -> rule1)) -> rule6)) -> rule4))]
("Dave" "is" "cold" "+")
((((((((triple6) -> (rule7 % int4)) triple6) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Dave is red.
("Dave" "is" "red" "+")
int4
Dave is not cold.
False
6
inv-proof
[(((((((((triple6) -> rule7) triple6) -> rule1)) -> rule6)) -> rule4))]
("Dave" "is" "cold" "-")
((((((((triple6) -> (rule7 % int4)) triple6) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Dave is red.
("Dave" "is" "red" "+")
int4
Dave is nice.
True
9
proof
[(((((((((((triple6) -> rule7) triple6) -> rule1)) -> rule6)) -> rule4) ((triple6) -> rule7)) -> rule5))]
("Dave" "is" "nice" "+")
((((((((((triple6) -> (rule7 % int5)) triple6) -> (rule1 % int4))) -> (rule6 % int3))) -> (rule4 % int2)) ((triple6) -> (rule7 % int5))) -> (rule5 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Dave is young.
("Dave" "is" "young" "+")
int4
Dave is red.
("Dave" "is" "red" "+")
int5
Dave is not nice.
False
9
inv-proof
[(((((((((((triple6) -> rule7) triple6) -> rule1)) -> rule6)) -> rule4) ((triple6) -> rule7)) -> rule5))]
("Dave" "is" "nice" "-")
((((((((((triple6) -> (rule7 % int5)) triple6) -> (rule1 % int4))) -> (rule6 % int3))) -> (rule4 % int2)) ((triple6) -> (rule7 % int5))) -> (rule5 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Dave is young.
("Dave" "is" "young" "+")
int4
Dave is red.
("Dave" "is" "red" "+")
int5
Bob is not green.
Unknown
inv-rconc
[@1: Bob is green.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Bob" "is" "green" "-")
Bob is young.
Unknown
rconc
[@1: Bob is young.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "young" "+")
Anne is not young.
Unknown
inv-rconc
[@1: Anne is young.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "young" "-")
Bob is cold.
Unknown
rconc
[@2: Bob is cold.[CWA. Example of deepest failure = (rule4 <- rule8 <- FAIL)]]
("Bob" "is" "cold" "+")
Harry is not cold.
Unknown
inv-rconc
[@1: Harry is cold.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Harry" "is" "cold" "-")
Harry is nice.
Unknown
rconc
[@2: Harry is nice.[CWA. Example of deepest failure = (rule5 <- rule4 <- FAIL)]]
("Harry" "is" "nice" "+")
Bob is not kind.
Unknown
inv-random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "-")
Anne is rough.
Unknown
random
[@0: Anne is rough.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "rough" "+")
Dave is not rough.
Unknown
inv-random
[@0: Dave is rough.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "rough" "-")
Bob is rough.
Unknown
random
[@0: Bob is rough.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "rough" "+")
Anne is not green.
Unknown
inv-random
[@0: Anne is green.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "green" "-")
Anne is kind.
Unknown
random
[@0: Anne is kind.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "kind" "+")
@0: Anne is nice.[(triple2)] Anne is not cold.[(triple1)] Anne is red.[(triple3)] Bob is nice.[(triple4)] Bob is not red.[(triple5)] Dave is kind.[(triple6)] Harry is not green.[(triple7)] Harry is not kind.[(triple8 OR ((triple10) -> rule3))] Harry is red.[(triple9)] Harry is rough.[(triple10)] Harry is young.[(triple11)] @1: Dave is red.[(((triple6) -> rule7))] @2: Dave is young.[(((((triple6) -> rule7) triple6) -> rule1))] @3: Dave is green.[(((((((triple6) -> rule7) triple6) -> rule1)) -> rule6))] @4: Dave is cold.[(((((((((triple6) -> rule7) triple6) -> rule1)) -> rule6)) -> rule4))] @5: Dave is nice.[(((((((((((triple6) -> rule7) triple6) -> rule1)) -> rule6)) -> rule4) ((triple6) -> rule7)) -> rule5))]
Anne is nice.
("Anne" "is" "nice" "+")
triple2
Anne is not cold.
("Anne" "is" "cold" "-")
triple1
Anne is red.
("Anne" "is" "red" "+")
triple3
Bob is nice.
("Bob" "is" "nice" "+")
triple4
Bob is not red.
("Bob" "is" "red" "-")
triple5
Dave is kind.
("Dave" "is" "kind" "+")
triple6
Harry is not green.
("Harry" "is" "green" "-")
triple7
Harry is not kind.
("Harry" "is" "kind" "-")
triple8
((triple10) -> (rule3 % int1))
Harry is not kind.
("Harry" "is" "kind" "-")
int1
Harry is red.
("Harry" "is" "red" "+")
triple9
Harry is rough.
("Harry" "is" "rough" "+")
triple10
Harry is young.
("Harry" "is" "young" "+")
triple11
Dave is red.
("Dave" "is" "red" "+")
((triple6) -> (rule7 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
((((triple6) -> (rule7 % int2)) triple6) -> (rule1 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
((((((triple6) -> (rule7 % int3)) triple6) -> (rule1 % int2))) -> (rule6 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
Dave is cold.
("Dave" "is" "cold" "+")
((((((((triple6) -> (rule7 % int4)) triple6) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Dave is red.
("Dave" "is" "red" "+")
int4
Dave is nice.
("Dave" "is" "nice" "+")
((((((((((triple6) -> (rule7 % int5)) triple6) -> (rule1 % int4))) -> (rule6 % int3))) -> (rule4 % int2)) ((triple6) -> (rule7 % int5))) -> (rule5 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Dave is young.
("Dave" "is" "young" "+")
int4
Dave is red.
("Dave" "is" "red" "+")
int5