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