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