Dave is furry. Erin is quiet. Fiona is red. Gary is furry. If something is rough then it is round. If Gary is furry then Gary is big. If something is rough then it is nice. All nice, big things are furry. All furry things are red. All big, furry things are nice. Red things are big. All nice, big things are rough.
Dave is furry.
("Dave" "is" "furry" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Gary is furry.
("Gary" "is" "furry" "+")
If something is rough then it is round.
((("something" "is" "rough" "+")) -> ("something" "is" "round" "+"))
If Gary is furry then Gary is big.
((("Gary" "is" "furry" "+")) -> ("Gary" "is" "big" "+"))
If something is rough then it is nice.
((("something" "is" "rough" "+")) -> ("something" "is" "nice" "+"))
All nice, big things are furry.
((("something" "is" "nice" "+") ("something" "is" "big" "+")) -> ("something" "is" "furry" "+"))
All furry things are red.
((("something" "is" "furry" "+")) -> ("something" "is" "red" "+"))
All big, furry things are nice.
((("something" "is" "big" "+") ("something" "is" "furry" "+")) -> ("something" "is" "nice" "+"))
Red things are big.
((("something" "is" "red" "+")) -> ("something" "is" "big" "+"))
All nice, big things are rough.
((("something" "is" "nice" "+") ("something" "is" "big" "+")) -> ("something" "is" "rough" "+"))
Gary is furry.
True
1
proof
[(triple4)]
("Gary" "is" "furry" "+")
triple4
Gary is not furry.
False
1
inv-proof
[(triple4)]
("Gary" "is" "furry" "-")
triple4
Fiona is not furry.
Unknown
inv-rconc
[@4: Fiona is furry.[CWA. Example of deepest failure = (rule4 <- rule3 <- rule8 <- rule6 <- FAIL)]]
("Fiona" "is" "furry" "-")
Dave is quiet.
Unknown
random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "+")
@0: Dave is furry.[(triple1)] Erin is quiet.[(triple2)] Fiona is red.[(triple3)] Gary is furry.[(triple4)] @1: Dave is red.[(((triple1) -> rule5))] Fiona is big.[(((triple3) -> rule7))] Gary is big.[(((triple4) -> rule2) OR ((((triple4) -> rule5)) -> rule7))] Gary is red.[(((triple4) -> rule5))] @2: Dave is big.[(((((triple1) -> rule5)) -> rule7))] Gary is nice.[(((((triple4) -> rule2) triple4) -> rule6) OR ((((((triple4) -> rule5)) -> rule7) triple4) -> rule6))] @3: Dave is nice.[(((((((triple1) -> rule5)) -> rule7) triple1) -> rule6))] Gary is rough.[(((((((triple4) -> rule2) triple4) -> rule6) ((triple4) -> rule2)) -> rule8) OR ((((((triple4) -> rule2) triple4) -> rule6) ((((triple4) -> rule5)) -> rule7)) -> rule8) OR ((((((((triple4) -> rule5)) -> rule7) triple4) -> rule6) ((triple4) -> rule2)) -> rule8) OR ((((((((triple4) -> rule5)) -> rule7) triple4) -> rule6) ((((triple4) -> rule5)) -> rule7)) -> rule8))] @4: Dave is rough.[(((((((((triple1) -> rule5)) -> rule7) triple1) -> rule6) ((((triple1) -> rule5)) -> rule7)) -> rule8))] Gary is round.[(((((((((triple4) -> rule2) triple4) -> rule6) ((triple4) -> rule2)) -> rule8)) -> rule1) OR ((((((((triple4) -> rule2) triple4) -> rule6) ((((triple4) -> rule5)) -> rule7)) -> rule8)) -> rule1) OR ((((((((((triple4) -> rule5)) -> rule7) triple4) -> rule6) ((triple4) -> rule2)) -> rule8)) -> rule1) OR ((((((((((triple4) -> rule5)) -> rule7) triple4) -> rule6) ((((triple4) -> rule5)) -> rule7)) -> rule8)) -> rule1))] @5: Dave is round.[(((((((((((triple1) -> rule5)) -> rule7) triple1) -> rule6) ((((triple1) -> rule5)) -> rule7)) -> rule8)) -> rule1))]
Dave is furry.
("Dave" "is" "furry" "+")
triple1
Erin is quiet.
("Erin" "is" "quiet" "+")
triple2
Fiona is red.
("Fiona" "is" "red" "+")
triple3
Gary is furry.
("Gary" "is" "furry" "+")
triple4
Dave is red.
("Dave" "is" "red" "+")
((triple1) -> (rule5 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
((triple3) -> (rule7 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
((triple4) -> (rule2 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
((((triple4) -> (rule5 % int2))) -> (rule7 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
((triple4) -> (rule5 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
((((triple1) -> (rule5 % int2))) -> (rule7 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
((((triple4) -> (rule2 % int2)) triple4) -> (rule6 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
((((((triple4) -> (rule5 % int3))) -> (rule7 % int2)) triple4) -> (rule6 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
Dave is nice.
("Dave" "is" "nice" "+")
((((((triple1) -> (rule5 % int3))) -> (rule7 % int2)) triple1) -> (rule6 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
Gary is rough.
("Gary" "is" "rough" "+")
((((((triple4) -> (rule2 % int3)) triple4) -> (rule6 % int2)) ((triple4) -> (rule2 % int3))) -> (rule8 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
((((((triple4) -> (rule2 % int4)) triple4) -> (rule6 % int3)) ((((triple4) -> (rule5 % int2))) -> (rule7 % int4))) -> (rule8 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
Gary is big.
("Gary" "is" "big" "+")
int4
((((((((triple4) -> (rule5 % int4))) -> (rule7 % int3)) triple4) -> (rule6 % int2)) ((triple4) -> (rule2 % int3))) -> (rule8 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
Gary is red.
("Gary" "is" "red" "+")
int4
((((((((triple4) -> (rule5 % int4))) -> (rule7 % int3)) triple4) -> (rule6 % int2)) ((((triple4) -> (rule5 % int4))) -> (rule7 % int3))) -> (rule8 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
Gary is red.
("Gary" "is" "red" "+")
int4
Dave is rough.
("Dave" "is" "rough" "+")
((((((((triple1) -> (rule5 % int4))) -> (rule7 % int3)) triple1) -> (rule6 % int2)) ((((triple1) -> (rule5 % int4))) -> (rule7 % int3))) -> (rule8 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is red.
("Dave" "is" "red" "+")
int4
Gary is round.
("Gary" "is" "round" "+")
((((((((triple4) -> (rule2 % int4)) triple4) -> (rule6 % int3)) ((triple4) -> (rule2 % int4))) -> (rule8 % int2))) -> (rule1 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
Gary is big.
("Gary" "is" "big" "+")
int4
((((((((triple4) -> (rule2 % int5)) triple4) -> (rule6 % int4)) ((((triple4) -> (rule5 % int3))) -> (rule7 % int5))) -> (rule8 % int2))) -> (rule1 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
Gary is nice.
("Gary" "is" "nice" "+")
int4
Gary is big.
("Gary" "is" "big" "+")
int5
((((((((((triple4) -> (rule5 % int5))) -> (rule7 % int4)) triple4) -> (rule6 % int3)) ((triple4) -> (rule2 % int4))) -> (rule8 % int2))) -> (rule1 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
Gary is big.
("Gary" "is" "big" "+")
int4
Gary is red.
("Gary" "is" "red" "+")
int5
((((((((((triple4) -> (rule5 % int5))) -> (rule7 % int4)) triple4) -> (rule6 % int3)) ((((triple4) -> (rule5 % int5))) -> (rule7 % int4))) -> (rule8 % int2))) -> (rule1 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
Gary is big.
("Gary" "is" "big" "+")
int4
Gary is red.
("Gary" "is" "red" "+")
int5
Dave is round.
("Dave" "is" "round" "+")
((((((((((triple1) -> (rule5 % int5))) -> (rule7 % int4)) triple1) -> (rule6 % int3)) ((((triple1) -> (rule5 % int5))) -> (rule7 % int4))) -> (rule8 % int2))) -> (rule1 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is big.
("Dave" "is" "big" "+")
int4
Dave is red.
("Dave" "is" "red" "+")
int5