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