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