Charlie is smart. Dave is rough. Gary is round. Harry is young. All round, young things are rough. If something is smart and rough then it is young. If something is smart and round then it is rough. If Dave is rough and Dave is blue then Dave is smart. Furry things are blue. All round things are smart. If Dave is rough and Dave is smart then Dave is round. If Gary is smart then Gary is rough.
Charlie is smart.
("Charlie" "is" "smart" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Gary is round.
("Gary" "is" "round" "+")
Harry is young.
("Harry" "is" "young" "+")
All round, young things are rough.
((("something" "is" "round" "+") ("something" "is" "young" "+")) -> ("something" "is" "rough" "+"))
If something is smart and rough then it is young.
((("something" "is" "smart" "+") ("something" "is" "rough" "+")) -> ("something" "is" "young" "+"))
If something is smart and round then it is rough.
((("something" "is" "smart" "+") ("something" "is" "round" "+")) -> ("something" "is" "rough" "+"))
If Dave is rough and Dave is blue then Dave is smart.
((("Dave" "is" "rough" "+") ("Dave" "is" "blue" "+")) -> ("Dave" "is" "smart" "+"))
Furry things are blue.
((("something" "is" "furry" "+")) -> ("something" "is" "blue" "+"))
All round things are smart.
((("something" "is" "round" "+")) -> ("something" "is" "smart" "+"))
If Dave is rough and Dave is smart then Dave is round.
((("Dave" "is" "rough" "+") ("Dave" "is" "smart" "+")) -> ("Dave" "is" "round" "+"))
If Gary is smart then Gary is rough.
((("Gary" "is" "smart" "+")) -> ("Gary" "is" "rough" "+"))
Gary is round.
True
1
proof
[(triple3)]
("Gary" "is" "round" "+")
triple3
Gary is not round.
False
1
inv-proof
[(triple3)]
("Gary" "is" "round" "-")
triple3
Gary is smart.
True
2
proof
[(((triple3) -> rule6))]
("Gary" "is" "smart" "+")
((triple3) -> (rule6 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is not smart.
False
2
inv-proof
[(((triple3) -> rule6))]
("Gary" "is" "smart" "-")
((triple3) -> (rule6 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is rough.
True
3
proof
[(((((triple3) -> rule6)) -> rule8) OR ((((triple3) -> rule6) triple3) -> rule3))]
("Gary" "is" "rough" "+")
((((triple3) -> (rule6 % int2))) -> (rule8 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
((((triple3) -> (rule6 % int2)) triple3) -> (rule3 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is not rough.
False
3
inv-proof
[(((((triple3) -> rule6)) -> rule8) OR ((((triple3) -> rule6) triple3) -> rule3))]
("Gary" "is" "rough" "-")
((((triple3) -> (rule6 % int2))) -> (rule8 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
((((triple3) -> (rule6 % int2)) triple3) -> (rule3 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Dave is not round.
Unknown
inv-rconc
[@3: Dave is round.[CWA. Example of deepest failure = (rule7 <- rule4 <- rule5 <- FAIL)]]
("Dave" "is" "round" "-")
Dave is blue.
Unknown
rconc
[@1: Dave is blue.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Dave" "is" "blue" "+")
Charlie is not blue.
Unknown
inv-rconc
[@1: Charlie is blue.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Charlie" "is" "blue" "-")
Harry is furry.
Unknown
random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "+")
Charlie is not green.
Unknown
inv-random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "-")
Harry is round.
Unknown
random
[@0: Harry is round.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "round" "+")
@0: Charlie is smart.[(triple1)] Dave is rough.[(triple2)] Gary is round.[(triple3)] Harry is young.[(triple4)] @1: Gary is smart.[(((triple3) -> rule6))] @2: Gary is rough.[(((((triple3) -> rule6)) -> rule8) OR ((((triple3) -> rule6) triple3) -> rule3))] @3: Gary is young.[(((((triple3) -> rule6) ((((triple3) -> rule6)) -> rule8)) -> rule2) OR ((((triple3) -> rule6) ((((triple3) -> rule6) triple3) -> rule3)) -> rule2))]
Charlie is smart.
("Charlie" "is" "smart" "+")
triple1
Dave is rough.
("Dave" "is" "rough" "+")
triple2
Gary is round.
("Gary" "is" "round" "+")
triple3
Harry is young.
("Harry" "is" "young" "+")
triple4
Gary is smart.
("Gary" "is" "smart" "+")
((triple3) -> (rule6 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
((((triple3) -> (rule6 % int2))) -> (rule8 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
((((triple3) -> (rule6 % int2)) triple3) -> (rule3 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
((((triple3) -> (rule6 % int3)) ((((triple3) -> (rule6 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
((((triple3) -> (rule6 % int3)) ((((triple3) -> (rule6 % int3)) triple3) -> (rule3 % int2))) -> (rule2 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3