Anne is quiet. Charlie is red. Harry is cold. All red, rough things are big. If Charlie is big then Charlie is quiet. If something is nice and cold then it is white. All quiet, nice things are rough. If something is red then it is big. White things are big. If something is quiet then it is rough. If something is quiet and red then it is rough.
Anne is quiet.
("Anne" "is" "quiet" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Harry is cold.
("Harry" "is" "cold" "+")
All red, rough things are big.
((("something" "is" "red" "+") ("something" "is" "rough" "+")) -> ("something" "is" "big" "+"))
If Charlie is big then Charlie is quiet.
((("Charlie" "is" "big" "+")) -> ("Charlie" "is" "quiet" "+"))
If something is nice and cold then it is white.
((("something" "is" "nice" "+") ("something" "is" "cold" "+")) -> ("something" "is" "white" "+"))
All quiet, nice things are rough.
((("something" "is" "quiet" "+") ("something" "is" "nice" "+")) -> ("something" "is" "rough" "+"))
If something is red then it is big.
((("something" "is" "red" "+")) -> ("something" "is" "big" "+"))
White things are big.
((("something" "is" "white" "+")) -> ("something" "is" "big" "+"))
If something is quiet then it is rough.
((("something" "is" "quiet" "+")) -> ("something" "is" "rough" "+"))
If something is quiet and red then it is rough.
((("something" "is" "quiet" "+") ("something" "is" "red" "+")) -> ("something" "is" "rough" "+"))
Anne is quiet.
True
1
proof
[(triple1)]
("Anne" "is" "quiet" "+")
triple1
Anne is not quiet.
False
1
inv-proof
[(triple1)]
("Anne" "is" "quiet" "-")
triple1
Anne is rough.
True
2
proof
[(((triple1) -> rule7))]
("Anne" "is" "rough" "+")
((triple1) -> (rule7 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Charlie is not big.
False
2
inv-proof
[(((triple2) -> rule5))]
("Charlie" "is" "big" "-")
((triple2) -> (rule5 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is quiet.
True
3
proof
[(((((triple2) -> rule5)) -> rule2))]
("Charlie" "is" "quiet" "+")
((((triple2) -> (rule5 % int2))) -> (rule2 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is not quiet.
False
3
inv-proof
[(((((triple2) -> rule5)) -> rule2))]
("Charlie" "is" "quiet" "-")
((((triple2) -> (rule5 % int2))) -> (rule2 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is rough.
True
4
proof
[(((((((triple2) -> rule5)) -> rule2)) -> rule7) OR ((((((triple2) -> rule5)) -> rule2) triple2) -> rule8))]
("Charlie" "is" "rough" "+")
((((((triple2) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
((((((triple2) -> (rule5 % int3))) -> (rule2 % int2)) triple2) -> (rule8 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Charlie is not rough.
False
4
inv-proof
[(((((((triple2) -> rule5)) -> rule2)) -> rule7) OR ((((((triple2) -> rule5)) -> rule2) triple2) -> rule8))]
("Charlie" "is" "rough" "-")
((((((triple2) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
((((((triple2) -> (rule5 % int3))) -> (rule2 % int2)) triple2) -> (rule8 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Charlie is not white.
Unknown
inv-rconc
[@1: Charlie is white.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "white" "-")
Harry is big.
Unknown
rconc
[@2: Harry is big.[CWA. Example of deepest failure = (rule6 <- rule3 <- FAIL)]]
("Harry" "is" "big" "+")
Harry is not rough.
Unknown
inv-rconc
[@1: Harry is rough.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Harry" "is" "rough" "-")
Anne is big.
Unknown
rconc
[@2: Anne is big.[CWA. Example of deepest failure = (rule6 <- rule3 <- FAIL)]]
("Anne" "is" "big" "+")
Harry is not quiet.
Unknown
inv-random
[@0: Harry is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "quiet" "-")
Charlie is cold.
Unknown
random
[@0: Charlie is cold.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "cold" "+")
Charlie is not nice.
Unknown
inv-random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "-")
Anne is cold.
Unknown
random
[@0: Anne is cold.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "cold" "+")
@0: Anne is quiet.[(triple1)] Charlie is red.[(triple2)] Harry is cold.[(triple3)] @1: Anne is rough.[(((triple1) -> rule7))] Charlie is big.[(((triple2) -> rule5))] @2: Charlie is quiet.[(((((triple2) -> rule5)) -> rule2))] @3: Charlie is rough.[(((((((triple2) -> rule5)) -> rule2)) -> rule7) OR ((((((triple2) -> rule5)) -> rule2) triple2) -> rule8))]
Anne is quiet.
("Anne" "is" "quiet" "+")
triple1
Charlie is red.
("Charlie" "is" "red" "+")
triple2
Harry is cold.
("Harry" "is" "cold" "+")
triple3
Anne is rough.
("Anne" "is" "rough" "+")
((triple1) -> (rule7 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
((triple2) -> (rule5 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((((triple2) -> (rule5 % int2))) -> (rule2 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
((((((triple2) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
((((((triple2) -> (rule5 % int3))) -> (rule2 % int2)) triple2) -> (rule8 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3