Anne is quiet. Anne is smart. Anne is not white. Charlie is furry. Charlie is not quiet. Charlie is rough. Charlie is white. Erin is not blue. Erin is not quiet. Gary is big. Gary is furry. Gary is not quiet. Gary is rough. Gary is smart. Gary is white. If Anne is smart and Anne is white then Anne is quiet. If something is big and blue then it is white. Furry, rough things are white. If Gary is rough and Gary is white then Gary is big. Big things are smart. If Erin is big and Erin is blue then Erin is not furry. All white things are big. If something is rough and not white then it is quiet.
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Anne is not white.
("Anne" "is" "white" "-")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Erin is not blue.
("Erin" "is" "blue" "-")
Erin is not quiet.
("Erin" "is" "quiet" "-")
Gary is big.
("Gary" "is" "big" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is not quiet.
("Gary" "is" "quiet" "-")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is white.
("Gary" "is" "white" "+")
If Anne is smart and Anne is white then Anne is quiet.
((("Anne" "is" "smart" "+") ("Anne" "is" "white" "+")) -> ("Anne" "is" "quiet" "+"))
If something is big and blue then it is white.
((("something" "is" "big" "+") ("something" "is" "blue" "+")) -> ("something" "is" "white" "+"))
Furry, rough things are white.
((("something" "is" "furry" "+") ("something" "is" "rough" "+")) -> ("something" "is" "white" "+"))
If Gary is rough and Gary is white then Gary is big.
((("Gary" "is" "rough" "+") ("Gary" "is" "white" "+")) -> ("Gary" "is" "big" "+"))
Big things are smart.
((("something" "is" "big" "+")) -> ("something" "is" "smart" "+"))
If Erin is big and Erin is blue then Erin is not furry.
((("Erin" "is" "big" "+") ("Erin" "is" "blue" "+")) -> ("Erin" "is" "furry" "-"))
All white things are big.
((("something" "is" "white" "+")) -> ("something" "is" "big" "+"))
If something is rough and not white then it is quiet.
((("something" "is" "rough" "+") ("something" "is" "white" "~")) -> ("something" "is" "quiet" "+"))
Gary is furry.
True
1
proof
[(triple11)]
("Gary" "is" "furry" "+")
triple11
Gary is not rough.
False
1
inv-proof
[(triple13)]
("Gary" "is" "rough" "-")
triple13
Charlie is big.
True
2
proof
[(((triple7) -> rule7) OR ((((triple4 triple6) -> rule3)) -> rule7))]
("Charlie" "is" "big" "+")
((triple7) -> (rule7 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
((((triple4 triple6) -> (rule3 % int2))) -> (rule7 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is not big.
False
2
inv-proof
[(((triple7) -> rule7) OR ((((triple4 triple6) -> rule3)) -> rule7))]
("Charlie" "is" "big" "-")
((triple7) -> (rule7 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
((((triple4 triple6) -> (rule3 % int2))) -> (rule7 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is smart.
True
3
proof
[(((((triple7) -> rule7)) -> rule5) OR ((((((triple4 triple6) -> rule3)) -> rule7)) -> rule5))]
("Charlie" "is" "smart" "+")
((((triple7) -> (rule7 % int2))) -> (rule5 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
((((((triple4 triple6) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
Charlie is not smart.
False
3
inv-proof
[(((((triple7) -> rule7)) -> rule5) OR ((((((triple4 triple6) -> rule3)) -> rule7)) -> rule5))]
("Charlie" "is" "smart" "-")
((((triple7) -> (rule7 % int2))) -> (rule5 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
((((((triple4 triple6) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
Erin is not white.
Unknown
inv-rconc
[@1: Erin is white.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Erin" "is" "white" "-")
Erin is big.
Unknown
rconc
[@2: Erin is big.[CWA. Example of deepest failure = (rule7 <- rule2 <- FAIL)]]
("Erin" "is" "big" "+")
Anne is not big.
Unknown
inv-rconc
[@1: Anne is big.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Anne" "is" "big" "-")
Anne is furry.
Unknown
random
[@0: Anne is furry.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "furry" "+")
Gary is not blue.
Unknown
inv-random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "-")
Charlie is blue.
Unknown
random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "+")
@0: Anne is not white.[(triple3)] Anne is quiet.[(triple1)] Anne is smart.[(triple2)] Charlie is furry.[(triple4)] Charlie is not quiet.[(triple5)] Charlie is rough.[(triple6)] Charlie is white.[(triple7 OR ((triple4 triple6) -> rule3))] Erin is not blue.[(triple8)] Erin is not quiet.[(triple9)] Gary is big.[(triple10 OR ((triple15) -> rule7) OR ((triple13 triple15) -> rule4) OR ((((triple11 triple13) -> rule3)) -> rule7) OR ((triple13 ((triple11 triple13) -> rule3)) -> rule4))] Gary is furry.[(triple11)] Gary is not quiet.[(triple12)] Gary is rough.[(triple13)] Gary is smart.[(triple14 OR ((triple10) -> rule5) OR ((((triple15) -> rule7)) -> rule5) OR ((((triple13 triple15) -> rule4)) -> rule5) OR ((((((triple11 triple13) -> rule3)) -> rule7)) -> rule5) OR ((((triple13 ((triple11 triple13) -> rule3)) -> rule4)) -> rule5))] Gary is white.[(triple15 OR ((triple11 triple13) -> rule3))] @1: Charlie is big.[(((triple7) -> rule7) OR ((((triple4 triple6) -> rule3)) -> rule7))] @2: Charlie is smart.[(((((triple7) -> rule7)) -> rule5) OR ((((((triple4 triple6) -> rule3)) -> rule7)) -> rule5))]
Anne is not white.
("Anne" "is" "white" "-")
triple3
Anne is quiet.
("Anne" "is" "quiet" "+")
triple1
Anne is smart.
("Anne" "is" "smart" "+")
triple2
Charlie is furry.
("Charlie" "is" "furry" "+")
triple4
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
triple5
Charlie is rough.
("Charlie" "is" "rough" "+")
triple6
Charlie is white.
("Charlie" "is" "white" "+")
triple7
((triple4 triple6) -> (rule3 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Erin is not blue.
("Erin" "is" "blue" "-")
triple8
Erin is not quiet.
("Erin" "is" "quiet" "-")
triple9
Gary is big.
("Gary" "is" "big" "+")
triple10
((triple15) -> (rule7 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
((triple13 triple15) -> (rule4 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
((((triple11 triple13) -> (rule3 % int2))) -> (rule7 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
((triple13 ((triple11 triple13) -> (rule3 % int2))) -> (rule4 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
triple11
Gary is not quiet.
("Gary" "is" "quiet" "-")
triple12
Gary is rough.
("Gary" "is" "rough" "+")
triple13
Gary is smart.
("Gary" "is" "smart" "+")
triple14
((triple10) -> (rule5 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
((((triple15) -> (rule7 % int2))) -> (rule5 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
((((triple13 triple15) -> (rule4 % int2))) -> (rule5 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
((((((triple11 triple13) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
((((triple13 ((triple11 triple13) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Gary is white.
("Gary" "is" "white" "+")
triple15
((triple11 triple13) -> (rule3 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
((triple7) -> (rule7 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
((((triple4 triple6) -> (rule3 % int2))) -> (rule7 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
((((triple7) -> (rule7 % int2))) -> (rule5 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
((((((triple4 triple6) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3