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