Charlie is young. Dave is nice. Gary is big. Gary is round. Harry is not big. Harry is rough. Harry is not round. If Dave is rough and Dave is big then Dave is white. If something is round then it is furry. If something is rough and nice then it is big. If something is rough and young then it is big. If something is nice then it is round. If something is rough and big then it is not round. If something is furry and nice then it is white. If something is white then it is young. All white, young things are not rough.
Charlie is young.
("Charlie" "is" "young" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is round.
("Gary" "is" "round" "+")
Harry is not big.
("Harry" "is" "big" "-")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is not round.
("Harry" "is" "round" "-")
If Dave is rough and Dave is big then Dave is white.
((("Dave" "is" "rough" "+") ("Dave" "is" "big" "+")) -> ("Dave" "is" "white" "+"))
If something is round then it is furry.
((("something" "is" "round" "+")) -> ("something" "is" "furry" "+"))
If something is rough and nice then it is big.
((("something" "is" "rough" "+") ("something" "is" "nice" "+")) -> ("something" "is" "big" "+"))
If something is rough and young then it is big.
((("something" "is" "rough" "+") ("something" "is" "young" "+")) -> ("something" "is" "big" "+"))
If something is nice then it is round.
((("something" "is" "nice" "+")) -> ("something" "is" "round" "+"))
If something is rough and big then it is not round.
((("something" "is" "rough" "+") ("something" "is" "big" "+")) -> ("something" "is" "round" "-"))
If something is furry and nice then it is white.
((("something" "is" "furry" "+") ("something" "is" "nice" "+")) -> ("something" "is" "white" "+"))
If something is white then it is young.
((("something" "is" "white" "+")) -> ("something" "is" "young" "+"))
All white, young things are not rough.
((("something" "is" "white" "+") ("something" "is" "young" "+")) -> ("something" "is" "rough" "-"))
Harry is rough.
True
1
proof
[(triple6)]
("Harry" "is" "rough" "+")
triple6
Harry is big.
False
1
inv-proof
[(triple5)]
("Harry" "is" "big" "+")
triple5
Dave is round.
True
2
proof
[(((triple2) -> rule5))]
("Dave" "is" "round" "+")
((triple2) -> (rule5 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Gary is not furry.
False
2
inv-proof
[(((triple4) -> rule2))]
("Gary" "is" "furry" "-")
((triple4) -> (rule2 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Dave is furry.
True
3
proof
[(((((triple2) -> rule5)) -> rule2))]
("Dave" "is" "furry" "+")
((((triple2) -> (rule5 % int2))) -> (rule2 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is not furry.
False
3
inv-proof
[(((((triple2) -> rule5)) -> rule2))]
("Dave" "is" "furry" "-")
((((triple2) -> (rule5 % int2))) -> (rule2 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is white.
True
5
proof
[(((((((triple2) -> rule5)) -> rule2) triple2) -> rule7))]
("Dave" "is" "white" "+")
((((((triple2) -> (rule5 % int3))) -> (rule2 % int2)) triple2) -> (rule7 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is not white.
False
5
inv-proof
[(((((((triple2) -> rule5)) -> rule2) triple2) -> rule7))]
("Dave" "is" "white" "-")
((((((triple2) -> (rule5 % int3))) -> (rule2 % int2)) triple2) -> (rule7 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is young.
True
6
proof
[(((((((((triple2) -> rule5)) -> rule2) triple2) -> rule7)) -> rule8))]
("Dave" "is" "young" "+")
((((((((triple2) -> (rule5 % int4))) -> (rule2 % int3)) triple2) -> (rule7 % int2))) -> (rule8 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Dave is round.
("Dave" "is" "round" "+")
int4
Dave is not young.
False
6
inv-proof
[(((((((((triple2) -> rule5)) -> rule2) triple2) -> rule7)) -> rule8))]
("Dave" "is" "young" "-")
((((((((triple2) -> (rule5 % int4))) -> (rule2 % int3)) triple2) -> (rule7 % int2))) -> (rule8 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Dave is round.
("Dave" "is" "round" "+")
int4
Dave is not rough.
True
12
proof
[(((((((((triple2) -> rule5)) -> rule2) triple2) -> rule7) ((((((((triple2) -> rule5)) -> rule2) triple2) -> rule7)) -> rule8)) -> rule9))]
("Dave" "is" "rough" "-")
((((((((triple2) -> (rule5 % int5))) -> (rule2 % int4)) triple2) -> (rule7 % int3)) ((((((((triple2) -> (rule5 % int5))) -> (rule2 % int4)) triple2) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule9 % int1))
Dave is not rough.
("Dave" "is" "rough" "-")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Dave is furry.
("Dave" "is" "furry" "+")
int4
Dave is round.
("Dave" "is" "round" "+")
int5
Dave is rough.
False
12
inv-proof
[(((((((((triple2) -> rule5)) -> rule2) triple2) -> rule7) ((((((((triple2) -> rule5)) -> rule2) triple2) -> rule7)) -> rule8)) -> rule9))]
("Dave" "is" "rough" "+")
((((((((triple2) -> (rule5 % int5))) -> (rule2 % int4)) triple2) -> (rule7 % int3)) ((((((((triple2) -> (rule5 % int5))) -> (rule2 % int4)) triple2) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule9 % int1))
Dave is not rough.
("Dave" "is" "rough" "-")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Dave is furry.
("Dave" "is" "furry" "+")
int4
Dave is round.
("Dave" "is" "round" "+")
int5
Gary is not young.
Unknown
inv-rconc
[@2: Gary is young.[CWA. Example of deepest failure = (rule8 <- rule7 <- FAIL)]]
("Gary" "is" "young" "-")
Charlie is furry.
Unknown
rconc
[@2: Charlie is furry.[CWA. Example of deepest failure = (rule2 <- rule5 <- FAIL)]]
("Charlie" "is" "furry" "+")
Dave is not big.
Unknown
inv-rconc
[@1: Dave is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "big" "-")
Charlie is round.
Unknown
rconc
[@1: Charlie is round.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Charlie" "is" "round" "+")
Charlie is not big.
Unknown
inv-rconc
[@1: Charlie is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "big" "-")
Gary is white.
Unknown
rconc
[@1: Gary is white.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Gary" "is" "white" "+")
Charlie is not nice.
Unknown
inv-random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "-")
Harry is nice.
Unknown
random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "+")
Gary is not nice.
Unknown
inv-random
[@0: Gary is nice.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "nice" "-")
Charlie is rough.
Unknown
random
[@0: Charlie is rough.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "rough" "+")
@0: Charlie is young.[(triple1)] Dave is nice.[(triple2)] Gary is big.[(triple3)] Gary is round.[(triple4)] Harry is not big.[(triple5)] Harry is not round.[(triple7)] Harry is rough.[(triple6)] @1: Dave is round.[(((triple2) -> rule5))] Gary is furry.[(((triple4) -> rule2))] @2: Dave is furry.[(((((triple2) -> rule5)) -> rule2))] @3: Dave is white.[(((((((triple2) -> rule5)) -> rule2) triple2) -> rule7))] @4: Dave is young.[(((((((((triple2) -> rule5)) -> rule2) triple2) -> rule7)) -> rule8))] @5: Dave is not rough.[(((((((((triple2) -> rule5)) -> rule2) triple2) -> rule7) ((((((((triple2) -> rule5)) -> rule2) triple2) -> rule7)) -> rule8)) -> rule9))]
Charlie is young.
("Charlie" "is" "young" "+")
triple1
Dave is nice.
("Dave" "is" "nice" "+")
triple2
Gary is big.
("Gary" "is" "big" "+")
triple3
Gary is round.
("Gary" "is" "round" "+")
triple4
Harry is not big.
("Harry" "is" "big" "-")
triple5
Harry is not round.
("Harry" "is" "round" "-")
triple7
Harry is rough.
("Harry" "is" "rough" "+")
triple6
Dave is round.
("Dave" "is" "round" "+")
((triple2) -> (rule5 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
((triple4) -> (rule2 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
((((triple2) -> (rule5 % int2))) -> (rule2 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
((((((triple2) -> (rule5 % int3))) -> (rule2 % int2)) triple2) -> (rule7 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is young.
("Dave" "is" "young" "+")
((((((((triple2) -> (rule5 % int4))) -> (rule2 % int3)) triple2) -> (rule7 % int2))) -> (rule8 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Dave is round.
("Dave" "is" "round" "+")
int4
Dave is not rough.
("Dave" "is" "rough" "-")
((((((((triple2) -> (rule5 % int5))) -> (rule2 % int4)) triple2) -> (rule7 % int3)) ((((((((triple2) -> (rule5 % int5))) -> (rule2 % int4)) triple2) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule9 % int1))
Dave is not rough.
("Dave" "is" "rough" "-")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Dave is furry.
("Dave" "is" "furry" "+")
int4
Dave is round.
("Dave" "is" "round" "+")
int5