Anne is rough. Charlie is nice. Charlie is not smart. Dave is smart. Harry is cold. Harry is green. Harry is quiet. Quiet, rough things are green. Smart things are quiet. If Anne is rough and Anne is green then Anne is not nice. All rough things are cold. Rough, green things are cold. All quiet things are smart. Cold things are smart. If something is nice then it is furry. If something is cold then it is furry.
Anne is rough.
("Anne" "is" "rough" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is not smart.
("Charlie" "is" "smart" "-")
Dave is smart.
("Dave" "is" "smart" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Quiet, rough things are green.
((("something" "is" "quiet" "+") ("something" "is" "rough" "+")) -> ("something" "is" "green" "+"))
Smart things are quiet.
((("something" "is" "smart" "+")) -> ("something" "is" "quiet" "+"))
If Anne is rough and Anne is green then Anne is not nice.
((("Anne" "is" "rough" "+") ("Anne" "is" "green" "+")) -> ("Anne" "is" "nice" "-"))
All rough things are cold.
((("something" "is" "rough" "+")) -> ("something" "is" "cold" "+"))
Rough, green things are cold.
((("something" "is" "rough" "+") ("something" "is" "green" "+")) -> ("something" "is" "cold" "+"))
All quiet things are smart.
((("something" "is" "quiet" "+")) -> ("something" "is" "smart" "+"))
Cold things are smart.
((("something" "is" "cold" "+")) -> ("something" "is" "smart" "+"))
If something is nice then it is furry.
((("something" "is" "nice" "+")) -> ("something" "is" "furry" "+"))
If something is cold then it is furry.
((("something" "is" "cold" "+")) -> ("something" "is" "furry" "+"))
Dave is smart.
True
1
proof
[(triple4)]
("Dave" "is" "smart" "+")
triple4
Charlie is not nice.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "nice" "-")
triple2
Harry is furry.
True
2
proof
[(((triple5) -> rule9))]
("Harry" "is" "furry" "+")
((triple5) -> (rule9 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Anne is not cold.
False
2
inv-proof
[(((triple1) -> rule4))]
("Anne" "is" "cold" "-")
((triple1) -> (rule4 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is smart.
True
3
proof
[(((((triple1) -> rule4)) -> rule7))]
("Anne" "is" "smart" "+")
((((triple1) -> (rule4 % int2))) -> (rule7 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is not smart.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule7))]
("Anne" "is" "smart" "-")
((((triple1) -> (rule4 % int2))) -> (rule7 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is quiet.
True
4
proof
[(((((((triple1) -> rule4)) -> rule7)) -> rule2))]
("Anne" "is" "quiet" "+")
((((((triple1) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Anne is not quiet.
False
4
inv-proof
[(((((((triple1) -> rule4)) -> rule7)) -> rule2))]
("Anne" "is" "quiet" "-")
((((((triple1) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Anne is green.
True
6
proof
[(((((((((triple1) -> rule4)) -> rule7)) -> rule2) triple1) -> rule1))]
("Anne" "is" "green" "+")
((((((((triple1) -> (rule4 % int4))) -> (rule7 % int3))) -> (rule2 % int2)) triple1) -> (rule1 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is cold.
("Anne" "is" "cold" "+")
int4
Anne is not green.
False
6
inv-proof
[(((((((((triple1) -> rule4)) -> rule7)) -> rule2) triple1) -> rule1))]
("Anne" "is" "green" "-")
((((((((triple1) -> (rule4 % int4))) -> (rule7 % int3))) -> (rule2 % int2)) triple1) -> (rule1 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is cold.
("Anne" "is" "cold" "+")
int4
Anne is not nice.
True
8
proof
[(((triple1 ((((((((triple1) -> rule4)) -> rule7)) -> rule2) triple1) -> rule1)) -> rule3))]
("Anne" "is" "nice" "-")
((triple1 ((((((((triple1) -> (rule4 % int5))) -> (rule7 % int4))) -> (rule2 % int3)) triple1) -> (rule1 % int2))) -> (rule3 % int1))
Anne is not nice.
("Anne" "is" "nice" "-")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
Anne is smart.
("Anne" "is" "smart" "+")
int4
Anne is cold.
("Anne" "is" "cold" "+")
int5
Anne is nice.
False
8
inv-proof
[(((triple1 ((((((((triple1) -> rule4)) -> rule7)) -> rule2) triple1) -> rule1)) -> rule3))]
("Anne" "is" "nice" "+")
((triple1 ((((((((triple1) -> (rule4 % int5))) -> (rule7 % int4))) -> (rule2 % int3)) triple1) -> (rule1 % int2))) -> (rule3 % int1))
Anne is not nice.
("Anne" "is" "nice" "-")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
Anne is smart.
("Anne" "is" "smart" "+")
int4
Anne is cold.
("Anne" "is" "cold" "+")
int5
Charlie is not quiet.
Unknown
inv-rconc
[@1: Charlie is quiet.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "quiet" "-")
Dave is cold.
Unknown
rconc
[@1: Dave is cold.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Dave" "is" "cold" "+")
Dave is not furry.
Unknown
inv-rconc
[@2: Dave is furry.[CWA. Example of deepest failure = (rule9 <- rule4 <- FAIL)]]
("Dave" "is" "furry" "-")
Charlie is cold.
Unknown
rconc
[@1: Charlie is cold.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Charlie" "is" "cold" "+")
Charlie is not green.
Unknown
inv-rconc
[@1: Charlie is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "green" "-")
Dave is green.
Unknown
rconc
[@1: Dave is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "green" "+")
Dave is not rough.
Unknown
inv-random
[@0: Dave is rough.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "rough" "-")
Charlie is rough.
Unknown
random
[@0: Charlie is rough.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "rough" "+")
Dave is not nice.
Unknown
inv-random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "-")
Harry is nice.
Unknown
random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "+")
@0: Anne is rough.[(triple1)] Charlie is nice.[(triple2)] Charlie is not smart.[(triple3)] Dave is smart.[(triple4)] Harry is cold.[(triple5)] Harry is green.[(triple6)] Harry is quiet.[(triple7 OR ((((triple5) -> rule7)) -> rule2))] @1: Anne is cold.[(((triple1) -> rule4))] Charlie is furry.[(((triple2) -> rule8))] Dave is quiet.[(((triple4) -> rule2))] Harry is furry.[(((triple5) -> rule9))] Harry is smart.[(((triple5) -> rule7) OR ((triple7) -> rule6))] @2: Anne is furry.[(((((triple1) -> rule4)) -> rule9))] Anne is smart.[(((((triple1) -> rule4)) -> rule7))] @3: Anne is quiet.[(((((((triple1) -> rule4)) -> rule7)) -> rule2))] @4: Anne is green.[(((((((((triple1) -> rule4)) -> rule7)) -> rule2) triple1) -> rule1))] @5: Anne is not nice.[(((triple1 ((((((((triple1) -> rule4)) -> rule7)) -> rule2) triple1) -> rule1)) -> rule3))]
Anne is rough.
("Anne" "is" "rough" "+")
triple1
Charlie is nice.
("Charlie" "is" "nice" "+")
triple2
Charlie is not smart.
("Charlie" "is" "smart" "-")
triple3
Dave is smart.
("Dave" "is" "smart" "+")
triple4
Harry is cold.
("Harry" "is" "cold" "+")
triple5
Harry is green.
("Harry" "is" "green" "+")
triple6
Harry is quiet.
("Harry" "is" "quiet" "+")
triple7
((((triple5) -> (rule7 % int2))) -> (rule2 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
((triple1) -> (rule4 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
((triple2) -> (rule8 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
((triple4) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
((triple5) -> (rule9 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
((triple5) -> (rule7 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
((triple7) -> (rule6 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
((((triple1) -> (rule4 % int2))) -> (rule9 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
((((triple1) -> (rule4 % int2))) -> (rule7 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
((((((triple1) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Anne is green.
("Anne" "is" "green" "+")
((((((((triple1) -> (rule4 % int4))) -> (rule7 % int3))) -> (rule2 % int2)) triple1) -> (rule1 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is cold.
("Anne" "is" "cold" "+")
int4
Anne is not nice.
("Anne" "is" "nice" "-")
((triple1 ((((((((triple1) -> (rule4 % int5))) -> (rule7 % int4))) -> (rule2 % int3)) triple1) -> (rule1 % int2))) -> (rule3 % int1))
Anne is not nice.
("Anne" "is" "nice" "-")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
Anne is smart.
("Anne" "is" "smart" "+")
int4
Anne is cold.
("Anne" "is" "cold" "+")
int5