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