Anne is kind. Anne is quiet. Bob is kind. Bob is rough. Erin is nice. Gary is smart. Gary is young. All kind, young things are blue. Quiet, kind things are nice. If Bob is blue then Bob is nice. Nice things are quiet. All kind, nice things are quiet. Smart, rough things are young. Kind, rough things are smart. All rough, quiet things are young.
Anne is kind.
("Anne" "is" "kind" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is young.
("Gary" "is" "young" "+")
All kind, young things are blue.
((("something" "is" "kind" "+") ("something" "is" "young" "+")) -> ("something" "is" "blue" "+"))
Quiet, kind things are nice.
((("something" "is" "quiet" "+") ("something" "is" "kind" "+")) -> ("something" "is" "nice" "+"))
If Bob is blue then Bob is nice.
((("Bob" "is" "blue" "+")) -> ("Bob" "is" "nice" "+"))
Nice things are quiet.
((("something" "is" "nice" "+")) -> ("something" "is" "quiet" "+"))
All kind, nice things are quiet.
((("something" "is" "kind" "+") ("something" "is" "nice" "+")) -> ("something" "is" "quiet" "+"))
Smart, rough things are young.
((("something" "is" "smart" "+") ("something" "is" "rough" "+")) -> ("something" "is" "young" "+"))
Kind, rough things are smart.
((("something" "is" "kind" "+") ("something" "is" "rough" "+")) -> ("something" "is" "smart" "+"))
All rough, quiet things are young.
((("something" "is" "rough" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "young" "+"))
Erin is nice.
True
1
proof
[(triple5)]
("Erin" "is" "nice" "+")
triple5
Erin is not nice.
False
1
inv-proof
[(triple5)]
("Erin" "is" "nice" "-")
triple5
Erin is quiet.
True
2
proof
[(((triple5) -> rule4))]
("Erin" "is" "quiet" "+")
((triple5) -> (rule4 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Anne is not nice.
False
3
inv-proof
[(((triple2 triple1) -> rule2))]
("Anne" "is" "nice" "-")
((triple2 triple1) -> (rule2 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Bob is young.
True
5
proof
[(((((triple3 triple4) -> rule7) triple4) -> rule6))]
("Bob" "is" "young" "+")
((((triple3 triple4) -> (rule7 % int2)) triple4) -> (rule6 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is not young.
False
5
inv-proof
[(((((triple3 triple4) -> rule7) triple4) -> rule6))]
("Bob" "is" "young" "-")
((((triple3 triple4) -> (rule7 % int2)) triple4) -> (rule6 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is blue.
True
7
proof
[(((triple3 ((((triple3 triple4) -> rule7) triple4) -> rule6)) -> rule1))]
("Bob" "is" "blue" "+")
((triple3 ((((triple3 triple4) -> (rule7 % int3)) triple4) -> (rule6 % int2))) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Bob is not blue.
False
7
inv-proof
[(((triple3 ((((triple3 triple4) -> rule7) triple4) -> rule6)) -> rule1))]
("Bob" "is" "blue" "-")
((triple3 ((((triple3 triple4) -> (rule7 % int3)) triple4) -> (rule6 % int2))) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Bob is nice.
True
8
proof
[(((((triple3 ((((triple3 triple4) -> rule7) triple4) -> rule6)) -> rule1)) -> rule3))]
("Bob" "is" "nice" "+")
((((triple3 ((((triple3 triple4) -> (rule7 % int4)) triple4) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Bob is smart.
("Bob" "is" "smart" "+")
int4
Bob is not nice.
False
8
inv-proof
[(((((triple3 ((((triple3 triple4) -> rule7) triple4) -> rule6)) -> rule1)) -> rule3))]
("Bob" "is" "nice" "-")
((((triple3 ((((triple3 triple4) -> (rule7 % int4)) triple4) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Bob is smart.
("Bob" "is" "smart" "+")
int4
Bob is quiet.
True
9
proof
[(((((((triple3 ((((triple3 triple4) -> rule7) triple4) -> rule6)) -> rule1)) -> rule3)) -> rule4) OR ((triple3 ((((triple3 ((((triple3 triple4) -> rule7) triple4) -> rule6)) -> rule1)) -> rule3)) -> rule5))]
("Bob" "is" "quiet" "+")
((((((triple3 ((((triple3 triple4) -> (rule7 % int5)) triple4) -> (rule6 % int4))) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Bob is young.
("Bob" "is" "young" "+")
int4
Bob is smart.
("Bob" "is" "smart" "+")
int5
((triple3 ((((triple3 ((((triple3 triple4) -> (rule7 % int5)) triple4) -> (rule6 % int4))) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Bob is young.
("Bob" "is" "young" "+")
int4
Bob is smart.
("Bob" "is" "smart" "+")
int5
Bob is not quiet.
False
9
inv-proof
[(((((((triple3 ((((triple3 triple4) -> rule7) triple4) -> rule6)) -> rule1)) -> rule3)) -> rule4) OR ((triple3 ((((triple3 ((((triple3 triple4) -> rule7) triple4) -> rule6)) -> rule1)) -> rule3)) -> rule5))]
("Bob" "is" "quiet" "-")
((((((triple3 ((((triple3 triple4) -> (rule7 % int5)) triple4) -> (rule6 % int4))) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Bob is young.
("Bob" "is" "young" "+")
int4
Bob is smart.
("Bob" "is" "smart" "+")
int5
((triple3 ((((triple3 ((((triple3 triple4) -> (rule7 % int5)) triple4) -> (rule6 % int4))) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Bob is young.
("Bob" "is" "young" "+")
int4
Bob is smart.
("Bob" "is" "smart" "+")
int5
Anne is not smart.
Unknown
inv-rconc
[@1: Anne is smart.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Anne" "is" "smart" "-")
Anne is young.
Unknown
rconc
[@1: Anne is young.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Anne" "is" "young" "+")
Gary is not quiet.
Unknown
inv-rconc
[@2: Gary is quiet.[CWA. Example of deepest failure = (rule4 <- rule2 <- FAIL)]]
("Gary" "is" "quiet" "-")
Erin is young.
Unknown
rconc
[@1: Erin is young.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Erin" "is" "young" "+")
Gary is not blue.
Unknown
inv-rconc
[@1: Gary is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "blue" "-")
Anne is blue.
Unknown
rconc
[@2: Anne is blue.[CWA. Example of deepest failure = (rule1 <- rule6 <- FAIL)]]
("Anne" "is" "blue" "+")
Anne is not rough.
Unknown
inv-random
[@0: Anne is rough.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "rough" "-")
Gary is rough.
Unknown
random
[@0: Gary is rough.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "rough" "+")
Erin is not rough.
Unknown
inv-random
[@0: Erin is rough.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "rough" "-")
Gary is kind.
Unknown
random
[@0: Gary is kind.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "kind" "+")
@0: Anne is kind.[(triple1)] Anne is quiet.[(triple2)] Bob is kind.[(triple3)] Bob is rough.[(triple4)] Erin is nice.[(triple5)] Gary is smart.[(triple6)] Gary is young.[(triple7)] @1: Anne is nice.[(((triple2 triple1) -> rule2))] Bob is smart.[(((triple3 triple4) -> rule7))] Erin is quiet.[(((triple5) -> rule4))] @2: Bob is young.[(((((triple3 triple4) -> rule7) triple4) -> rule6))] @3: Bob is blue.[(((triple3 ((((triple3 triple4) -> rule7) triple4) -> rule6)) -> rule1))] @4: Bob is nice.[(((((triple3 ((((triple3 triple4) -> rule7) triple4) -> rule6)) -> rule1)) -> rule3))] @5: Bob is quiet.[(((((((triple3 ((((triple3 triple4) -> rule7) triple4) -> rule6)) -> rule1)) -> rule3)) -> rule4) OR ((triple3 ((((triple3 ((((triple3 triple4) -> rule7) triple4) -> rule6)) -> rule1)) -> rule3)) -> rule5))]
Anne is kind.
("Anne" "is" "kind" "+")
triple1
Anne is quiet.
("Anne" "is" "quiet" "+")
triple2
Bob is kind.
("Bob" "is" "kind" "+")
triple3
Bob is rough.
("Bob" "is" "rough" "+")
triple4
Erin is nice.
("Erin" "is" "nice" "+")
triple5
Gary is smart.
("Gary" "is" "smart" "+")
triple6
Gary is young.
("Gary" "is" "young" "+")
triple7
Anne is nice.
("Anne" "is" "nice" "+")
((triple2 triple1) -> (rule2 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
((triple3 triple4) -> (rule7 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
((triple5) -> (rule4 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
((((triple3 triple4) -> (rule7 % int2)) triple4) -> (rule6 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
((triple3 ((((triple3 triple4) -> (rule7 % int3)) triple4) -> (rule6 % int2))) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Bob is nice.
("Bob" "is" "nice" "+")
((((triple3 ((((triple3 triple4) -> (rule7 % int4)) triple4) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Bob is smart.
("Bob" "is" "smart" "+")
int4
Bob is quiet.
("Bob" "is" "quiet" "+")
((((((triple3 ((((triple3 triple4) -> (rule7 % int5)) triple4) -> (rule6 % int4))) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Bob is young.
("Bob" "is" "young" "+")
int4
Bob is smart.
("Bob" "is" "smart" "+")
int5
((triple3 ((((triple3 ((((triple3 triple4) -> (rule7 % int5)) triple4) -> (rule6 % int4))) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Bob is young.
("Bob" "is" "young" "+")
int4
Bob is smart.
("Bob" "is" "smart" "+")
int5