Anne is big. Anne is white. Bob is red. Erin is quiet. Erin is red. Erin is smart. Gary is not quiet. All smart, quiet people are red. If someone is white then they are rough. If someone is young and quiet then they are smart. Young people are smart. All smart, white people are quiet. If someone is rough then they are young. If Gary is white then Gary is smart.
Anne is big.
("Anne" "is" "big" "+")
Anne is white.
("Anne" "is" "white" "+")
Bob is red.
("Bob" "is" "red" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Gary is not quiet.
("Gary" "is" "quiet" "-")
All smart, quiet people are red.
((("someone" "is" "smart" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "red" "+"))
If someone is white then they are rough.
((("someone" "is" "white" "+")) -> ("someone" "is" "rough" "+"))
If someone is young and quiet then they are smart.
((("someone" "is" "young" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "smart" "+"))
Young people are smart.
((("someone" "is" "young" "+")) -> ("someone" "is" "smart" "+"))
All smart, white people are quiet.
((("someone" "is" "smart" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "quiet" "+"))
If someone is rough then they are young.
((("someone" "is" "rough" "+")) -> ("someone" "is" "young" "+"))
If Gary is white then Gary is smart.
((("Gary" "is" "white" "+")) -> ("Gary" "is" "smart" "+"))
Bob is red.
True
1
proof
[(triple3)]
("Bob" "is" "red" "+")
triple3
Anne is not white.
False
1
inv-proof
[(triple2)]
("Anne" "is" "white" "-")
triple2
Anne is rough.
True
2
proof
[(((triple2) -> rule2))]
("Anne" "is" "rough" "+")
((triple2) -> (rule2 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is not rough.
False
2
inv-proof
[(((triple2) -> rule2))]
("Anne" "is" "rough" "-")
((triple2) -> (rule2 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is young.
True
3
proof
[(((((triple2) -> rule2)) -> rule6))]
("Anne" "is" "young" "+")
((((triple2) -> (rule2 % int2))) -> (rule6 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is not young.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule6))]
("Anne" "is" "young" "-")
((((triple2) -> (rule2 % int2))) -> (rule6 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is smart.
True
4
proof
[(((((((triple2) -> rule2)) -> rule6)) -> rule4))]
("Anne" "is" "smart" "+")
((((((triple2) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
Anne is not smart.
False
4
inv-proof
[(((((((triple2) -> rule2)) -> rule6)) -> rule4))]
("Anne" "is" "smart" "-")
((((((triple2) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
Anne is quiet.
True
6
proof
[(((((((((triple2) -> rule2)) -> rule6)) -> rule4) triple2) -> rule5))]
("Anne" "is" "quiet" "+")
((((((((triple2) -> (rule2 % int4))) -> (rule6 % int3))) -> (rule4 % int2)) triple2) -> (rule5 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is rough.
("Anne" "is" "rough" "+")
int4
Anne is not quiet.
False
6
inv-proof
[(((((((((triple2) -> rule2)) -> rule6)) -> rule4) triple2) -> rule5))]
("Anne" "is" "quiet" "-")
((((((((triple2) -> (rule2 % int4))) -> (rule6 % int3))) -> (rule4 % int2)) triple2) -> (rule5 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is rough.
("Anne" "is" "rough" "+")
int4
Anne is red.
True
11
proof
[(((((((((triple2) -> rule2)) -> rule6)) -> rule4) ((((((((triple2) -> rule2)) -> rule6)) -> rule4) triple2) -> rule5)) -> rule1))]
("Anne" "is" "red" "+")
((((((((triple2) -> (rule2 % int5))) -> (rule6 % int4))) -> (rule4 % int3)) ((((((((triple2) -> (rule2 % int5))) -> (rule6 % int4))) -> (rule4 % int3)) triple2) -> (rule5 % int2))) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is young.
("Anne" "is" "young" "+")
int4
Anne is rough.
("Anne" "is" "rough" "+")
int5
Anne is not red.
False
11
inv-proof
[(((((((((triple2) -> rule2)) -> rule6)) -> rule4) ((((((((triple2) -> rule2)) -> rule6)) -> rule4) triple2) -> rule5)) -> rule1))]
("Anne" "is" "red" "-")
((((((((triple2) -> (rule2 % int5))) -> (rule6 % int4))) -> (rule4 % int3)) ((((((((triple2) -> (rule2 % int5))) -> (rule6 % int4))) -> (rule4 % int3)) triple2) -> (rule5 % int2))) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is young.
("Anne" "is" "young" "+")
int4
Anne is rough.
("Anne" "is" "rough" "+")
int5
Bob is not rough.
Unknown
inv-rconc
[@1: Bob is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "rough" "-")
Gary is rough.
Unknown
rconc
[@1: Gary is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "rough" "+")
Gary is not red.
Unknown
inv-rconc
[@1: Gary is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "red" "-")
Gary is young.
Unknown
rconc
[@2: Gary is young.[CWA. Example of deepest failure = (rule6 <- rule2 <- FAIL)]]
("Gary" "is" "young" "+")
Erin is not young.
Unknown
inv-rconc
[@2: Erin is young.[CWA. Example of deepest failure = (rule6 <- rule2 <- FAIL)]]
("Erin" "is" "young" "-")
Erin is rough.
Unknown
rconc
[@1: Erin is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Erin" "is" "rough" "+")
Bob is not big.
Unknown
inv-random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "-")
Gary is white.
Unknown
random
[@0: Gary is white.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "white" "+")
Erin is not white.
Unknown
inv-random
[@0: Erin is white.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "white" "-")
Bob is white.
Unknown
random
[@0: Bob is white.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "white" "+")
Gary is not big.
Unknown
inv-random
[@0: Gary is big.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "big" "-")
Erin is big.
Unknown
random
[@0: Erin is big.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "big" "+")
@0: Anne is big.[(triple1)] Anne is white.[(triple2)] Bob is red.[(triple3)] Erin is quiet.[(triple4)] Erin is red.[(triple5 OR ((triple6 triple4) -> rule1))] Erin is smart.[(triple6)] Gary is not quiet.[(triple7)] @1: Anne is rough.[(((triple2) -> rule2))] @2: Anne is young.[(((((triple2) -> rule2)) -> rule6))] @3: Anne is smart.[(((((((triple2) -> rule2)) -> rule6)) -> rule4))] @4: Anne is quiet.[(((((((((triple2) -> rule2)) -> rule6)) -> rule4) triple2) -> rule5))] @5: Anne is red.[(((((((((triple2) -> rule2)) -> rule6)) -> rule4) ((((((((triple2) -> rule2)) -> rule6)) -> rule4) triple2) -> rule5)) -> rule1))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is white.
("Anne" "is" "white" "+")
triple2
Bob is red.
("Bob" "is" "red" "+")
triple3
Erin is quiet.
("Erin" "is" "quiet" "+")
triple4
Erin is red.
("Erin" "is" "red" "+")
triple5
((triple6 triple4) -> (rule1 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
triple6
Gary is not quiet.
("Gary" "is" "quiet" "-")
triple7
Anne is rough.
("Anne" "is" "rough" "+")
((triple2) -> (rule2 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
((((triple2) -> (rule2 % int2))) -> (rule6 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
((((((triple2) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
Anne is quiet.
("Anne" "is" "quiet" "+")
((((((((triple2) -> (rule2 % int4))) -> (rule6 % int3))) -> (rule4 % int2)) triple2) -> (rule5 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is rough.
("Anne" "is" "rough" "+")
int4
Anne is red.
("Anne" "is" "red" "+")
((((((((triple2) -> (rule2 % int5))) -> (rule6 % int4))) -> (rule4 % int3)) ((((((((triple2) -> (rule2 % int5))) -> (rule6 % int4))) -> (rule4 % int3)) triple2) -> (rule5 % int2))) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is young.
("Anne" "is" "young" "+")
int4
Anne is rough.
("Anne" "is" "rough" "+")
int5