Bob is cold. Dave is not cold. Dave is kind. Dave is quiet. Dave is young. Gary is nice. Harry is rough. Quiet, rough people are young. If Gary is quiet and Gary is young then Gary is rough. If Harry is rough then Harry is young. If someone is nice then they are kind. If someone is quiet and rough then they are kind. Young people are blue. All nice, cold people are rough. Young, blue people are quiet. All kind, young people are not nice.
Bob is cold.
("Bob" "is" "cold" "+")
Dave is not cold.
("Dave" "is" "cold" "-")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is young.
("Dave" "is" "young" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Quiet, rough people are young.
((("someone" "is" "quiet" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "young" "+"))
If Gary is quiet and Gary is young then Gary is rough.
((("Gary" "is" "quiet" "+") ("Gary" "is" "young" "+")) -> ("Gary" "is" "rough" "+"))
If Harry is rough then Harry is young.
((("Harry" "is" "rough" "+")) -> ("Harry" "is" "young" "+"))
If someone is nice then they are kind.
((("someone" "is" "nice" "+")) -> ("someone" "is" "kind" "+"))
If someone is quiet and rough then they are kind.
((("someone" "is" "quiet" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "kind" "+"))
Young people are blue.
((("someone" "is" "young" "+")) -> ("someone" "is" "blue" "+"))
All nice, cold people are rough.
((("someone" "is" "nice" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "rough" "+"))
Young, blue people are quiet.
((("someone" "is" "young" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "quiet" "+"))
All kind, young people are not nice.
((("someone" "is" "kind" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "nice" "-"))
Dave is kind.
True
1
proof
[(triple3)]
("Dave" "is" "kind" "+")
triple3
Dave is cold.
False
1
inv-proof
[(triple2)]
("Dave" "is" "cold" "+")
triple2
Dave is blue.
True
2
proof
[(((triple5) -> rule6))]
("Dave" "is" "blue" "+")
((triple5) -> (rule6 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is not blue.
False
2
inv-proof
[(((triple5) -> rule6))]
("Dave" "is" "blue" "-")
((triple5) -> (rule6 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Harry is blue.
True
3
proof
[(((((triple7) -> rule3)) -> rule6))]
("Harry" "is" "blue" "+")
((((triple7) -> (rule3 % int2))) -> (rule6 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is not blue.
False
3
inv-proof
[(((((triple7) -> rule3)) -> rule6))]
("Harry" "is" "blue" "-")
((((triple7) -> (rule3 % int2))) -> (rule6 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is quiet.
True
6
proof
[(((((triple7) -> rule3) ((((triple7) -> rule3)) -> rule6)) -> rule8))]
("Harry" "is" "quiet" "+")
((((triple7) -> (rule3 % int3)) ((((triple7) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
Harry is not quiet.
False
6
inv-proof
[(((((triple7) -> rule3) ((((triple7) -> rule3)) -> rule6)) -> rule8))]
("Harry" "is" "quiet" "-")
((((triple7) -> (rule3 % int3)) ((((triple7) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
Harry is kind.
True
8
proof
[(((((((triple7) -> rule3) ((((triple7) -> rule3)) -> rule6)) -> rule8) triple7) -> rule5))]
("Harry" "is" "kind" "+")
((((((triple7) -> (rule3 % int4)) ((((triple7) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule8 % int2)) triple7) -> (rule5 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Harry is young.
("Harry" "is" "young" "+")
int4
Harry is not kind.
False
8
inv-proof
[(((((((triple7) -> rule3) ((((triple7) -> rule3)) -> rule6)) -> rule8) triple7) -> rule5))]
("Harry" "is" "kind" "-")
((((((triple7) -> (rule3 % int4)) ((((triple7) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule8 % int2)) triple7) -> (rule5 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Harry is young.
("Harry" "is" "young" "+")
int4
Harry is not nice.
True
11
proof
[(((((((((triple7) -> rule3) ((((triple7) -> rule3)) -> rule6)) -> rule8) triple7) -> rule5) ((triple7) -> rule3)) -> rule9))]
("Harry" "is" "nice" "-")
((((((((triple7) -> (rule3 % int5)) ((((triple7) -> (rule3 % int5))) -> (rule6 % int4))) -> (rule8 % int3)) triple7) -> (rule5 % int2)) ((triple7) -> (rule3 % int5))) -> (rule9 % int1))
Harry is not nice.
("Harry" "is" "nice" "-")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Harry is blue.
("Harry" "is" "blue" "+")
int4
Harry is young.
("Harry" "is" "young" "+")
int5
Harry is nice.
False
11
inv-proof
[(((((((((triple7) -> rule3) ((((triple7) -> rule3)) -> rule6)) -> rule8) triple7) -> rule5) ((triple7) -> rule3)) -> rule9))]
("Harry" "is" "nice" "+")
((((((((triple7) -> (rule3 % int5)) ((((triple7) -> (rule3 % int5))) -> (rule6 % int4))) -> (rule8 % int3)) triple7) -> (rule5 % int2)) ((triple7) -> (rule3 % int5))) -> (rule9 % int1))
Harry is not nice.
("Harry" "is" "nice" "-")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Harry is blue.
("Harry" "is" "blue" "+")
int4
Harry is young.
("Harry" "is" "young" "+")
int5
Bob is not young.
Unknown
inv-rconc
[@2: Bob is young.[CWA. Example of deepest failure = (rule1 <- rule8 <- FAIL)]]
("Bob" "is" "young" "-")
Gary is young.
Unknown
rconc
[@2: Gary is young.[CWA. Example of deepest failure = (rule1 <- rule8 <- FAIL)]]
("Gary" "is" "young" "+")
Gary is not quiet.
Unknown
inv-rconc
[@2: Gary is quiet.[CWA. Example of deepest failure = (rule8 <- rule1 <- FAIL)]]
("Gary" "is" "quiet" "-")
Dave is rough.
Unknown
rconc
[@1: Dave is rough.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Dave" "is" "rough" "+")
Bob is not rough.
Unknown
inv-rconc
[@1: Bob is rough.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Bob" "is" "rough" "-")
Gary is blue.
Unknown
rconc
[@3: Gary is blue.[CWA. Example of deepest failure = (rule6 <- rule1 <- rule8 <- FAIL)]]
("Gary" "is" "blue" "+")
Harry is not cold.
Unknown
inv-random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "-")
Bob is nice.
Unknown
random
[@0: Bob is nice.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "nice" "+")
@0: Bob is cold.[(triple1)] Dave is kind.[(triple3)] Dave is not cold.[(triple2)] Dave is quiet.[(triple4 OR ((triple5 ((triple5) -> rule6)) -> rule8))] Dave is young.[(triple5)] Gary is nice.[(triple6)] Harry is rough.[(triple7)] @1: Dave is blue.[(((triple5) -> rule6))] Dave is not nice.[(((triple3 triple5) -> rule9))] Gary is kind.[(((triple6) -> rule4))] Harry is young.[(((triple7) -> rule3))] @2: Harry is blue.[(((((triple7) -> rule3)) -> rule6))] @3: Harry is quiet.[(((((triple7) -> rule3) ((((triple7) -> rule3)) -> rule6)) -> rule8))] @4: Harry is kind.[(((((((triple7) -> rule3) ((((triple7) -> rule3)) -> rule6)) -> rule8) triple7) -> rule5))] @5: Harry is not nice.[(((((((((triple7) -> rule3) ((((triple7) -> rule3)) -> rule6)) -> rule8) triple7) -> rule5) ((triple7) -> rule3)) -> rule9))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
Dave is kind.
("Dave" "is" "kind" "+")
triple3
Dave is not cold.
("Dave" "is" "cold" "-")
triple2
Dave is quiet.
("Dave" "is" "quiet" "+")
triple4
((triple5 ((triple5) -> (rule6 % int2))) -> (rule8 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
triple5
Gary is nice.
("Gary" "is" "nice" "+")
triple6
Harry is rough.
("Harry" "is" "rough" "+")
triple7
Dave is blue.
("Dave" "is" "blue" "+")
((triple5) -> (rule6 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is not nice.
("Dave" "is" "nice" "-")
((triple3 triple5) -> (rule9 % int1))
Dave is not nice.
("Dave" "is" "nice" "-")
int1
Gary is kind.
("Gary" "is" "kind" "+")
((triple6) -> (rule4 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
((triple7) -> (rule3 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
((((triple7) -> (rule3 % int2))) -> (rule6 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
((((triple7) -> (rule3 % int3)) ((((triple7) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
Harry is kind.
("Harry" "is" "kind" "+")
((((((triple7) -> (rule3 % int4)) ((((triple7) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule8 % int2)) triple7) -> (rule5 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Harry is young.
("Harry" "is" "young" "+")
int4
Harry is not nice.
("Harry" "is" "nice" "-")
((((((((triple7) -> (rule3 % int5)) ((((triple7) -> (rule3 % int5))) -> (rule6 % int4))) -> (rule8 % int3)) triple7) -> (rule5 % int2)) ((triple7) -> (rule3 % int5))) -> (rule9 % int1))
Harry is not nice.
("Harry" "is" "nice" "-")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Harry is blue.
("Harry" "is" "blue" "+")
int4
Harry is young.
("Harry" "is" "young" "+")
int5